changeset 45212 | e87feee00a4c |
parent 44923 | b80108b346a9 |
child 47818 | 151d137f1095 |
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Thu Oct 20 09:48:00 2011 +0200 @@ -3,7 +3,7 @@ subsubsection "Static Scoping of Procedures, Dynamic of Variables" -type_synonym penv = "(name \<times> com) list" +type_synonym penv = "(pname \<times> com) list" inductive big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)