equal
deleted
inserted
replaced
1 theory Lift |
1 theory Lift |
2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Abs" "Perm" "Equivp" "Rsp" |
5 "Abs" "Perm" "Rsp" |
6 begin |
6 begin |
7 |
7 |
8 |
8 |
9 ML {* |
9 ML {* |
10 fun define_quotient_types binds tys alphas equivps ctxt = |
10 fun define_quotient_types binds tys alphas equivps ctxt = |