src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
changeset 44177 b4b5cbca2519
parent 43158 686fa0a0696e
child 44923 b80108b346a9
equal deleted inserted replaced
44176:eda112e9cdee 44177:b4b5cbca2519
     1 theory Procs_Dyn_Vars_Dyn imports Util 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 = "name \<Rightarrow> com"