author | nipkow |
Thu, 09 May 2013 02:42:51 +0200 | |
changeset 51923 | 3d772b0af856 |
parent 51921 | bbbacaef19a6 (current diff) |
parent 51922 | 4cf0b93f9639 (diff) |
child 51924 | e398ab28eaa7 |
--- 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