equal
deleted
inserted
replaced
1 theory Procs_Dyn_Vars_Dyn imports Procs |
1 theory Procs_Dyn_Vars_Dyn imports Procs |
2 begin |
2 begin |
3 |
3 |
4 subsubsection "Dynamic Scoping of Procedures and Variables" |
4 subsubsection "Dynamic Scoping of Procedures and Variables" |
5 |
5 |
6 type_synonym penv = "name \<Rightarrow> com" |
6 type_synonym penv = "pname \<Rightarrow> com" |
7 |
7 |
8 inductive |
8 inductive |
9 big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
9 big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
10 where |
10 where |
11 Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" | |
11 Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" | |