equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Munich |
3 Author: Markus Wenzel, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* HOL type definitions *} |
6 header {* HOL type definitions *} |
7 |
7 |
8 theory Typedef = Set |
8 theory Typedef |
9 files ("Tools/typedef_package.ML"): |
9 import Set |
|
10 files ("Tools/typedef_package.ML") |
|
11 begin |
10 |
12 |
11 locale type_definition = |
13 locale type_definition = |
12 fixes Rep and Abs and A |
14 fixes Rep and Abs and A |
13 assumes Rep: "Rep x \<in> A" |
15 assumes Rep: "Rep x \<in> A" |
14 and Rep_inverse: "Abs (Rep x) = x" |
16 and Rep_inverse: "Abs (Rep x) = x" |