--- a/src/HOL/IMP/Abs_Int_Tests.thy Sun Feb 05 16:53:20 2012 +0100
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Sun Feb 05 17:09:21 2012 +0100
@@ -52,9 +52,9 @@
DO ''x'' ::= Plus (V ''x'') (N 1)"
definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ ''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;