equal
deleted
inserted
replaced
1 theory Procs_Stat_Vars_Dyn imports Procs |
1 theory Procs_Stat_Vars_Dyn imports Procs |
2 begin |
2 begin |
3 |
3 |
4 subsubsection "Static Scoping of Procedures, Dynamic of Variables" |
4 subsubsection "Static Scoping of Procedures, Dynamic of Variables" |
5 |
5 |
6 type_synonym penv = "(name \<times> com) list" |
6 type_synonym penv = "(pname \<times> com) list" |
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" | |