equal
deleted
inserted
replaced
5 header {* HOL type definitions *} |
5 header {* HOL type definitions *} |
6 |
6 |
7 theory Typedef |
7 theory Typedef |
8 imports Set |
8 imports Set |
9 keywords "typedef" :: thy_goal and "morphisms" |
9 keywords "typedef" :: thy_goal and "morphisms" |
10 uses ("Tools/typedef.ML") |
|
11 begin |
10 begin |
12 |
11 |
13 locale type_definition = |
12 locale type_definition = |
14 fixes Rep and Abs and A |
13 fixes Rep and Abs and A |
15 assumes Rep: "Rep x \<in> A" |
14 assumes Rep: "Rep x \<in> A" |
107 qed |
106 qed |
108 qed |
107 qed |
109 |
108 |
110 end |
109 end |
111 |
110 |
112 use "Tools/typedef.ML" setup Typedef.setup |
111 ML_file "Tools/typedef.ML" setup Typedef.setup |
113 |
112 |
114 end |
113 end |