equal
deleted
inserted
replaced
57 [ Conv.rewr_conv @{thm eqvt_bound}, |
57 [ Conv.rewr_conv @{thm eqvt_bound}, |
58 eqvt_apply_conv ctxt |
58 eqvt_apply_conv ctxt |
59 then_conv Conv.comb_conv (eqvt_conv ctxt), |
59 then_conv Conv.comb_conv (eqvt_conv ctxt), |
60 eqvt_lambda_conv ctxt |
60 eqvt_lambda_conv ctxt |
61 then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt, |
61 then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt, |
62 More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_thms ctxt), |
62 More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_raw_thms ctxt), |
63 Conv.all_conv |
63 Conv.all_conv |
64 ] ct |
64 ] ct |
65 |
65 |
66 fun eqvt_tac ctxt = |
66 fun eqvt_tac ctxt = |
67 CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) |
67 CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) |