# HG changeset patch
# User nipkow
# Date 1357907089 -3600
# Node ID 5adc528be033efb93b389e8b6ed386597ba79a6e
# Parent  e8d641235191aa868ca9afc8650f7390a82f02b3# Parent  95a61264a6ab17aa1e5fc2c02371906d05dad8b2
merged

diff -r e8d641235191 -r 5adc528be033 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Fri Jan 11 13:24:16 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Fri Jan 11 13:24:49 2013 +0100
@@ -15,25 +15,25 @@
 definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
 
 text{* Collecting semantics: *}
-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)"
+
+value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 2) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 3) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 4) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 5) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 6) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 7) C0)"
+value "show_acom [''x''] (((step {<>}) ^^ 8) C0)"
 
 text{* Small-step semantics: *}
-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))"
-
+value "show_acom [''x''] (((step {}) ^^ 0) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 1) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 2) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 3) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 4) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 5) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 6) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 7) (step {<>} C0))"
+value "show_acom [''x''] (((step {}) ^^ 8) (step {<>} C0))"
 
 end