Merge branch 'master' into highprecision

vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java

@@ -90,11 +90,11 @@ protected void tearDown() throws Exception
 		/* 24 */ "(forall mk_(i, $any1):(int) * (int) &\n  1 in set dom m)\n",
 		/* 25 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} &\n    x in set dom m))\n",
 		/* 26 */ "(forall mk_(i, $any1):(int) * (int) &\n  (forall x in set {m(1), 2, 3} & (m(x) < i) =>\n    x in set dom m))\n",
-		/* 27 */ "(let x:int = m(1) in\n  1 in set dom m)\n",
+		/* 27 */ "1 in set dom m\n",
 		/* 28 */ "(let x:int = m(1) in\n  x in set dom m)\n",
-		/* 29 */ "(let local: int -> int local(x) == m(x) in\n  (forall x:int &\n    x in set dom m))\n",
-		/* 30 */ "(let x = m(1) in\n  1 in set dom m)\n",
-		/* 31 */ "(let x = m(1) in\n  (let y = m(2) in\n    2 in set dom m))\n",
+		/* 29 */ "(forall x:int &\n  x in set dom m)\n",
+		/* 30 */ "1 in set dom m\n",
+		/* 31 */ "(let x = m(1) in\n  2 in set dom m)\n",
 		/* 32 */ "(let x = m(1), y = m(2) in\n  x in set dom m)\n",
 		/* 33 */ "(let x = m(1), y = m(2) in\n  y in set dom m)\n",
 		/* 34 */ "exists1 x in set {1, 2, 3} & (x < 10)\n",
@@ -128,10 +128,10 @@ protected void tearDown() throws Exception
 		/* 62 */ "dom {1 |-> false} subset inds [2, true, 7.8]\n",
 		/* 63 */ "is_(([2, true, 7.8] ++ {1 |-> false}), seq of (bool | nat))\n",
 		/* 64 */ "(forall t:((nat) * (nat) * (nat)) | ((nat) * (nat)) &\n  is_(t, (nat) * (nat) * (nat)))\n",
-		/* 65 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    exists mk_(a, b):U & mk_(a, b) = u))\n",
-		/* 66 */ "(forall u:U &\n  (let mk_(a, b):U = u in\n    is_(u, (nat) * (nat))))\n",
+		/* 65 */ "(forall u:U &\n  exists mk_(a, b):U & mk_(a, b) = u)\n",
+		/* 66 */ "(forall u:U &\n  is_(u, (nat) * (nat)))\n",
 		/* 67 */ "(is_([1, 2, true], T1) and ((is_(1, bool)) and (is_(2, bool)))) or (is_([1, 2, true], T2) and inv_T2([1, 2, true]))\n",
-		/* 68 */ "(forall t:T1 | T2 &\n  (let x:T1 | T2 = [1, 2, 3, true] in\n    (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true]))))\n",
+		/* 68 */ "(forall t:T1 | T2 &\n  (is_([1, 2, 3, true], T1) and ((is_(1, bool)) and (is_(2, bool)) and (is_(3, bool)))) or (is_([1, 2, 3, true], T2) and inv_T2([1, 2, 3, true])))\n",
 		/* 69 */ "(forall a:T1 | T2 | int &\n  (is_(a, T1) and (is_(a, seq of bool))) or (is_(a, T2) and inv_T2(a)))\n",
 		/* 70 */ "is_({1 |-> \"2\"}, inmap nat1 to seq1 of char)\n",
 		/* 71 */ "(forall n:nat1, x:nat1 &\n  (not (n < 2) =>\n    (n - 1) > 0))\n",