| changeset 50986 | c54ea7f5418f |
| parent 50821 | 95a61264a6ab |
| child 51040 | faf7f0d4f9eb |
--- a/src/HOL/IMP/Collecting_Examples.thy Sat Jan 19 17:42:12 2013 +0100 +++ b/src/HOL/IMP/Collecting_Examples.thy Sat Jan 19 21:05:05 2013 +0100 @@ -12,7 +12,7 @@ DO ''x'' ::= Plus (V ''x'') (N 2)" definition C0 :: "state set acom" where "C0 = anno {} c" -definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)" +definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)" text{* Collecting semantics: *}