equal
deleted
inserted
replaced
1161 val i = 1 + fold Integer.max (map (fn p => |
1161 val i = 1 + fold Integer.max (map (fn p => |
1162 find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1; |
1162 find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1; |
1163 val (rrs', asm') = rules_of_prem ss prem' |
1163 val (rrs', asm') = rules_of_prem ss prem' |
1164 in mut_impc prems concl rrss asms (prem' :: prems') |
1164 in mut_impc prems concl rrss asms (prem' :: prems') |
1165 (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) |
1165 (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) |
1166 (Library.take (i, prems)) |
1166 ((uncurry take) (i, prems)) |
1167 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies |
1167 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies |
1168 (Library.drop (i, prems), concl))))) :: eqns) |
1168 ((uncurry drop) (i, prems), concl))))) :: eqns) |
1169 ss (length prems') ~1 |
1169 ss (length prems') ~1 |
1170 end |
1170 end |
1171 |
1171 |
1172 (*legacy code - only for backwards compatibility*) |
1172 (*legacy code - only for backwards compatibility*) |
1173 and nonmut_impc ct ss = |
1173 and nonmut_impc ct ss = |