changeset 41798 | c3aa3c87ef21 |
parent 32960 | 69916a850301 |
child 49171 | 3d7a695385f1 |
--- a/src/HOL/Nominal/Examples/Crary.thy Mon Feb 21 11:50:38 2011 +0100 +++ b/src/HOL/Nominal/Examples/Crary.thy Mon Feb 21 17:43:23 2011 +0100 @@ -25,8 +25,8 @@ | App "trm" "trm" ("App _ _" [110,110] 100) | Const "nat" -types Ctxt = "(name\<times>ty) list" -types Subst = "(name\<times>trm) list" +type_synonym Ctxt = "(name\<times>ty) list" +type_synonym Subst = "(name\<times>trm) list" lemma perm_ty[simp]: