changeset 47821 | b8c7eb0c2f89 |
parent 42603 | 996b0c14a430 |
child 47824 | d0181abdbdac |
47820:acc8ebf980ca | 47821:b8c7eb0c2f89 |
---|---|
4 |
4 |
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 "morphisms" |
|
9 uses ("Tools/typedef.ML") |
10 uses ("Tools/typedef.ML") |
10 begin |
11 begin |
11 |
12 |
12 locale type_definition = |
13 locale type_definition = |
13 fixes Rep and Abs and A |
14 fixes Rep and Abs and A |