changeset 41778 | 5f79a9e42507 |
parent 37956 | ee939247b2fb |
child 58249 | 180f1b3508ed |
--- a/src/HOL/Bali/Value.thy Fri Feb 18 16:22:27 2011 +0100 +++ b/src/HOL/Bali/Value.thy Fri Feb 18 16:36:42 2011 +0100 @@ -26,7 +26,7 @@ primrec the_Addr :: "val \<Rightarrow> loc" where "the_Addr (Addr a) = a" -types dyn_ty = "loc \<Rightarrow> ty option" +type_synonym dyn_ty = "loc \<Rightarrow> ty option" primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" where