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" "Equivp" "Rsp" "Attic/Fv" |
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 = |
64 in |
64 in |
65 rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) |
65 rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) |
66 end |
66 end |
67 *} |
67 *} |
68 |
68 |
|
69 |
|
70 |
|
71 |
69 ML {* |
72 ML {* |
70 fun define_fv_alpha_export dt binds bns ctxt = |
73 fun define_fv_alpha_export dt binds bns ctxt = |
71 let |
74 let |
72 val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = |
75 val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = |
73 define_fv dt binds bns ctxt; |
76 define_fv dt binds bns ctxt; |