equal
deleted
inserted
replaced
121 |> Simplifier.set_subgoaler asm_simp_tac |
121 |> Simplifier.set_subgoaler asm_simp_tac |
122 |> Simplifier.set_mksimps (mksimps mksimps_pairs) |
122 |> Simplifier.set_mksimps (mksimps mksimps_pairs) |
123 |> Simplifier.set_mkcong mk_meta_cong |
123 |> Simplifier.set_mkcong mk_meta_cong |
124 |> simpset_of; |
124 |> simpset_of; |
125 |
125 |
126 fun unfold_tac ths ctxt = |
126 fun unfold_tac ctxt ths = |
127 ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths)); |
127 ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths)); |
128 |
128 |
129 |
129 |
130 (*** integration of simplifier with classical reasoner ***) |
130 (*** integration of simplifier with classical reasoner ***) |
131 |
131 |