| changeset 41798 | c3aa3c87ef21 |
| parent 37362 | 017146b7d139 |
| child 53015 | a1119cf551e8 |
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Feb 21 11:50:38 2011 +0100 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Feb 21 17:43:23 2011 +0100 @@ -380,7 +380,7 @@ text {* Typing Contexts *} -types tctx = "(name\<times>ty) list" +type_synonym tctx = "(name\<times>ty) list" text {* Sub-Typing Contexts *}