diff -r dc5f5cfe6a09 -r f23dc7d16c0b src/HOL/IMP/Collecting_list.thy
--- a/src/HOL/IMP/Collecting_list.thy	Mon Jan 16 07:46:58 2012 +0100
+++ b/src/HOL/IMP/Collecting_list.thy	Mon Jan 16 07:55:10 2012 +0100
@@ -15,15 +15,21 @@
 "step S ({Inv} WHILE b DO c {P}) =
   {S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}"
 
-definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)"
+
+text{* Examples: *}
+
+definition "c = WHILE Less (V ''x'') (N 3)
+                DO ''x'' ::= Plus (V ''x'') (N 2)"
 definition "c0 = anno [] c"
 
 definition "show_acom xs = map_acom (map (show_state xs))"
 
+
 text{* Collecting semantics: *}
 
 value "show_acom [''x''] (((step [<>]) ^^ 6) c0)"
 
+
 text{* Small step semantics: *}
 
 value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))"