equal
deleted
inserted
replaced
31 |
31 |
32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
33 |
33 |
34 code_pred big_step . |
34 code_pred big_step . |
35 |
35 |
36 values "{map t [''x'', ''y'', ''z''] |t. |
36 values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}" |
37 [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}" |
|
38 |
|
39 values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}" |
|
40 |
37 |
41 end |
38 end |