# HG changeset patch
# User nipkow
# Date 1363023201 -3600
# Node ID 408271602165ecff1c40d64e212819bd8edc12b7
# Parent  1dff81cf425bdd17499e4e98dc510a2b96528426
tuned

diff -r 1dff81cf425b -r 408271602165 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Mon Mar 11 18:33:21 2013 +0100
@@ -8,12 +8,12 @@
 by simp
 
 text{* In order to display commands annotated with state sets,
-states must be translated into a printable format as lists of pairs,
+states must be translated into a printable format as sets of pairs,
 for a given set of variable names. This is what @{text show_acom} does: *}
 
 definition show_acom ::
-  "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where
-"show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)"
+  "vname set \<Rightarrow> state set acom \<Rightarrow> (vname*val)set set acom" where
+"show_acom X = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` X) ` S)"
 
 
 text{* The example: *}
@@ -23,24 +23,24 @@
 
 text{* Collecting semantics: *}
 
-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)"
+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 {<>} 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))"
+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