merged
authornipkow
Thu, 09 May 2013 02:42:51 +0200
changeset 51923 3d772b0af856
parent 51921 bbbacaef19a6 (current diff)
parent 51922 4cf0b93f9639 (diff)
child 51924 e398ab28eaa7
merged
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Wed May 08 19:16:43 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Thu May 09 02:42:51 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