| changeset 1774 | c34347ec7ab3 |
| parent 1685 | 721d92623c9d |
| child 1830 | 8db45a106569 |
| child 1837 | edc2a52cd457 |
| 1773:c0eac04ae3b4 | 1774:c34347ec7ab3 |
|---|---|
1 theory Lift |
1 theory Lift |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Eqvt" |
|
4 "../Nominal_General/Nominal2_Supp" |
|
5 "Abs" "Perm" "Fv" "Rsp" |
|
3 begin |
6 begin |
4 |
7 |
5 |
8 |
6 ML {* |
9 ML {* |
7 fun define_quotient_types binds tys alphas equivps ctxt = |
10 fun define_quotient_types binds tys alphas equivps ctxt = |