# HG changeset patch
# User nipkow
# Date 1346826779 -7200
# Node ID 53f954510a8cfeb07305b3e7c3dfb3b8ea3dd608
# Parent  5c8fefe0f103cc75690adf98e7d055dca90fcea1
tuned

diff -r 5c8fefe0f103 -r 53f954510a8c src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Wed Sep 05 00:58:54 2012 +0200
+++ b/src/HOL/IMP/ACom.thy	Wed Sep 05 08:32:59 2012 +0200
@@ -16,7 +16,7 @@
   If bexp 'a "('a acom)" 'a "('a acom)" 'a
     ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
   While 'a bexp 'a "('a acom)" 'a
-    ("({_}//WHILE _/ DO ({_}/ _)//{_})"  [0, 0, 0, 61, 0] 61)
+    ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
 "post (SKIP {P}) = P" |
diff -r 5c8fefe0f103 -r 53f954510a8c src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Wed Sep 05 00:58:54 2012 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Wed Sep 05 08:32:59 2012 +0200
@@ -21,20 +21,25 @@
 definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
 
 text{* Collecting semantics: *}
-value "show_acom [''x''] (((step {%x. 0}) ^^ 1) c0)"
-value "show_acom [''x''] (((step {%x. 0}) ^^ 2) c0)"
-value "show_acom [''x''] (((step {%x. 0}) ^^ 3) c0)"
-value "show_acom [''x''] (((step {%x. 0}) ^^ 4) c0)"
-value "show_acom [''x''] (((step {%x. 0}) ^^ 5) c0)"
-value "show_acom [''x''] (((step {%x. 0}) ^^ 6) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 1) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 2) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 3) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 4) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 5) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 6) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 7) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 8) c0)"
 
 text{* Small-step semantics: *}
-value "show_acom [''x''] (((step {}) ^^ 0) (step {%x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 1) (step {%x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 2) (step {%x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 3) (step {%x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 4) (step {%x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 5) (step {%x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 0) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 1) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 2) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 3) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 4) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 5) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 6) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 7) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 8) (step {\<lambda>x. 0} c0))"
 
 
 end