equal
deleted
inserted
replaced
162 |
162 |
163 fun finish_tac q = SUBGOAL (fn (_, i) => |
163 fun finish_tac q = SUBGOAL (fn (_, i) => |
164 (if q then I else TRY) (rtac TrueI i)); |
164 (if q then I else TRY) (rtac TrueI i)); |
165 |
165 |
166 fun cooper_tac elim add_ths del_ths ctxt = |
166 fun cooper_tac elim add_ths del_ths ctxt = |
167 let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths |
167 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths |
168 in |
168 in |
169 ObjectLogic.full_atomize_tac |
169 ObjectLogic.full_atomize_tac |
170 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
170 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
171 THEN_ALL_NEW simp_tac ss |
171 THEN_ALL_NEW simp_tac ss |
172 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
172 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |