168 ObjectLogic.full_atomize_tac |
168 ObjectLogic.full_atomize_tac |
169 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
169 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
170 THEN_ALL_NEW simp_tac ss |
170 THEN_ALL_NEW simp_tac ss |
171 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
171 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
172 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
172 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
173 THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt)) |
173 THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt)) |
174 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
174 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
175 THEN_ALL_NEW div_mod_tac ctxt |
175 THEN_ALL_NEW div_mod_tac ctxt |
176 THEN_ALL_NEW splits_tac ctxt |
176 THEN_ALL_NEW splits_tac ctxt |
177 THEN_ALL_NEW simp_tac ss |
177 THEN_ALL_NEW simp_tac ss |
178 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
178 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
179 THEN_ALL_NEW nat_to_int_tac ctxt |
179 THEN_ALL_NEW nat_to_int_tac ctxt |
180 THEN_ALL_NEW core_cooper_tac ctxt |
180 THEN_ALL_NEW (core_cooper_tac ctxt) |
181 THEN_ALL_NEW finish_tac elim |
181 THEN_ALL_NEW finish_tac elim |
182 end; |
182 end; |
183 |
183 |
184 end; |
184 end; |