equal
deleted
inserted
replaced
61 |
61 |
62 fun simpset_program thy some_ss program = |
62 fun simpset_program thy some_ss program = |
63 simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss); |
63 simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss); |
64 |
64 |
65 fun lift_ss_conv f ss ct = |
65 fun lift_ss_conv f ss ct = |
66 f (Proof_Context.init_global (theory_of_cterm ct) |> Simplifier.put_simpset ss |> set_trace) ct; |
66 f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct; |
67 |
67 |
68 fun rewrite_modulo thy some_ss program = |
68 fun rewrite_modulo thy some_ss program = |
69 lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program); |
69 lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program); |
70 |
70 |
71 fun conclude_tac thy some_ss = |
71 fun conclude_tac thy some_ss = |