# HG changeset patch # User nipkow # Date 1368060171 -7200 # Node ID 3d772b0af85688edf462e80e9d4d52838e01728a # Parent bbbacaef19a6b0b19191bf4b5000068a59d2f2c2# Parent 4cf0b93f96396bd36a0675c904b9a9612ce19979 merged diff -r bbbacaef19a6 -r 3d772b0af856 src/HOL/IMP/Abs_Int_Tests.thy --- 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