--- a/src/HOL/IMP/Abs_Int1_parity.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri May 17 08:19:52 2013 +0200
@@ -133,12 +133,12 @@
subsubsection "Tests"
definition "test1_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
value [code] "show_acom (the(AI_parity test1_parity))"
definition "test2_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"