# HG changeset patch
# User nipkow
# Date 1368007564 -7200
# Node ID 4cf0b93f96396bd36a0675c904b9a9612ce19979
# Parent  f964a98877131b620dadf0cf59675ea2dc51be59
tuned

diff -r f964a9887713 -r 4cf0b93f9639 src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Wed May 08 11:57:42 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Wed May 08 12:06:04 2013 +0200
@@ -63,6 +63,6 @@
 
 definition "test6_ivl =
  ''x'' ::= N 0;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+ WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
 
 end