| changeset 51019 | 146f63c3f024 |
| parent 47818 | 151d137f1095 |
| child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Sun Feb 03 17:31:33 2013 +0100 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Mon Feb 04 09:06:20 2013 +0100 @@ -33,9 +33,6 @@ code_pred big_step . -values "{map t [''x'', ''y'', ''z''] |t. - [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}" - -values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}" +values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}" end