diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int1_parity.thy
--- 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)"