--- a/src/HOL/IMP/Abs_Int_Tests.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Fri May 17 08:19:52 2013 +0200
@@ -8,8 +8,8 @@
text{* Straight line code: *}
definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= N 7;;
+ ''z'' ::= Plus (V ''y'') (N 2);;
''y'' ::= Plus (V ''x'') (N 0)"
text{* Conditional: *}
@@ -18,26 +18,26 @@
text{* Conditional, test is relevant: *}
definition "test3_const =
- ''x'' ::= N 42;
+ ''x'' ::= N 42;;
IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
text{* While: *}
definition "test4_const =
- ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
+ ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
text{* While, test is relevant: *}
definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+ ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
text{* Iteration is needed: *}
definition "test6_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
- WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+ ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
+ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
text{* For intervals: *}
definition "test1_ivl =
- ''y'' ::= N 7;
+ ''y'' ::= N 7;;
IF Less (V ''x'') (V ''y'')
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
@@ -47,22 +47,22 @@
DO ''x'' ::= Plus (V ''x'') (N 1)"
definition "test3_ivl =
- ''x'' ::= N 7;
+ ''x'' ::= N 7;;
WHILE Less (V ''x'') (N 100)
DO ''x'' ::= Plus (V ''x'') (N 1)"
definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
+ ''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N 1))"
definition "test5_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
+ ''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 1000)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+ DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
definition "test6_ivl =
- ''x'' ::= N 0;
+ ''x'' ::= N 0;;
WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
end