equal
deleted
inserted
replaced
88 Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp |
88 Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp |
89 (big_rec_tm,pred))))) |
89 (big_rec_tm,pred))))) |
90 (fn prems => |
90 (fn prems => |
91 [rtac (impI RS allI) 1, |
91 [rtac (impI RS allI) 1, |
92 DETERM (etac Intr_elim.raw_induct 1), |
92 DETERM (etac Intr_elim.raw_induct 1), |
93 asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1, |
93 asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1, |
94 REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] |
94 REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] |
95 ORELSE' hyp_subst_tac)), |
95 ORELSE' hyp_subst_tac)), |
96 ind_tac (rev prems) (length prems)]) |
96 ind_tac (rev prems) (length prems)]) |
97 handle e => print_sign_exn sign e; |
97 handle e => print_sign_exn sign e; |
98 |
98 |