| changeset 15131 | c69542757a4d |
| parent 13421 | 8fcdf4a26468 |
| child 15140 | 322485b816ac |
--- a/src/HOL/Typedef.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Typedef.thy Mon Aug 16 14:22:27 2004 +0200 @@ -5,8 +5,10 @@ header {* HOL type definitions *} -theory Typedef = Set -files ("Tools/typedef_package.ML"): +theory Typedef +import Set +files ("Tools/typedef_package.ML") +begin locale type_definition = fixes Rep and Abs and A