equal
deleted
inserted
replaced
141 Ind_Syntax.mk_tprop |
141 Ind_Syntax.mk_tprop |
142 (Ind_Syntax.mk_all_imp |
142 (Ind_Syntax.mk_all_imp |
143 (big_rec_tm, |
143 (big_rec_tm, |
144 Abs("z", Ind_Syntax.iT, |
144 Abs("z", Ind_Syntax.iT, |
145 fold_bal (app Ind_Syntax.conj) |
145 fold_bal (app Ind_Syntax.conj) |
146 (map mk_rec_imp (Inductive.rec_tms~~preds))))) |
146 (ListPair.map mk_rec_imp (Inductive.rec_tms,preds))))) |
147 and mutual_induct_concl = |
147 and mutual_induct_concl = |
148 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
148 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
149 |
149 |
150 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], |
150 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], |
151 resolve_tac [allI, impI, conjI, Part_eqI], |
151 resolve_tac [allI, impI, conjI, Part_eqI], |