1.1 --- a/src/HOL/IMP/AExp.thy	Wed Feb 13 09:04:47 2013 +0100
     1.2 +++ b/src/HOL/IMP/AExp.thy	Wed Feb 13 11:28:44 2013 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  syntax 
     1.5    "_State" :: "updbinds => 'a" ("<_>")
     1.6  translations
     1.7 -  "_State ms" => "_Update <> ms"
     1.8 +  "_State ms" == "_Update <> ms"
     1.9  
    1.10  text {* \noindent
    1.11    We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:

     2.1 --- a/src/HOL/IMP/Collecting_Examples.thy	Wed Feb 13 09:04:47 2013 +0100
     2.2 +++ b/src/HOL/IMP/Collecting_Examples.thy	Wed Feb 13 11:28:44 2013 +0100
     2.3 @@ -7,13 +7,20 @@
     2.4  lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
     2.5  by simp
     2.6  
     2.7 +text{* In order to display commands annotated with state sets,
     2.8 +states must be translated into a printable format as lists of pairs,
     2.9 +for a given set of variable names. This is what @{text show_acom} does: *}
    2.10 +
    2.11 +definition show_acom ::
    2.12 +  "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where
    2.13 +"show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)"
    2.14 +
    2.15 +
    2.16  text{* The example: *}
    2.17  definition "c = WHILE Less (V ''x'') (N 3)
    2.18                  DO ''x'' ::= Plus (V ''x'') (N 2)"
    2.19  definition C0 :: "state set acom" where "C0 = anno {} c"
    2.20  
    2.21 -definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)"
    2.22 -
    2.23  text{* Collecting semantics: *}
    2.24  
    2.25  value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"