--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Wed Sep 14 06:49:01 2011 +0200
@@ -31,10 +31,9 @@
code_pred big_step .
-(* FIXME: example state syntax *)
values "{map t [''x'',''y'',''z''] |t.
- (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
+ (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
+values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
end