equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>HOL type definitions\<close> |
5 section \<open>HOL type definitions\<close> |
6 |
6 |
7 theory Typedef |
7 theory Typedef |
8 imports Set |
8 imports Set |
9 keywords "typedef" :: thy_goal and "morphisms" |
9 keywords |
|
10 "typedef" :: thy_goal and |
|
11 "morphisms" :: quasi_command |
10 begin |
12 begin |
11 |
13 |
12 locale type_definition = |
14 locale type_definition = |
13 fixes Rep and Abs and A |
15 fixes Rep and Abs and A |
14 assumes Rep: "Rep x \<in> A" |
16 assumes Rep: "Rep x \<in> A" |