| changeset 16417 | 9bc16273c2d4 |
| parent 15260 | a12e999a0113 |
| child 19459 | 2041d472fc17 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
5 |
5 |
6 header {* HOL type definitions *} |
6 header {* HOL type definitions *} |
7 |
7 |
8 theory Typedef |
8 theory Typedef |
9 imports Set |
9 imports Set |
10 files ("Tools/typedef_package.ML") |
10 uses ("Tools/typedef_package.ML") |
11 begin |
11 begin |
12 |
12 |
13 locale type_definition = |
13 locale type_definition = |
14 fixes Rep and Abs and A |
14 fixes Rep and Abs and A |
15 assumes Rep: "Rep x \<in> A" |
15 assumes Rep: "Rep x \<in> A" |