--- 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