src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
changeset 52201 146f63c3f024
parent 48689 151d137f1095
child 53183 bc01725d7918
     1.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Sun Feb 03 17:31:33 2013 +0100
     1.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Mon Feb 04 09:06:20 2013 +0100
     1.3 @@ -31,9 +31,6 @@
     1.4  
     1.5  code_pred big_step .
     1.6  
     1.7 -values "{map t [''x'',''y'',''z''] |t. 
     1.8 -          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
     1.9 -
    1.10 -values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
    1.11 +values "{map t [''x'',''y''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
    1.12  
    1.13  end