588 in case prop of |
588 in case prop of |
589 imp$A$B => |
589 imp$A$B => |
590 if imp=implies andalso A aconv propA |
590 if imp=implies andalso A aconv propA |
591 then |
591 then |
592 Thm{sign_ref= merge_thm_sgs(thAB,thA), |
592 Thm{sign_ref= merge_thm_sgs(thAB,thA), |
593 der = Pt.infer_derivs (curry Pt.%) der derA, |
593 der = Pt.infer_derivs (curry Pt.%%) der derA, |
594 maxidx = Int.max(maxA,maxidx), |
594 maxidx = Int.max(maxA,maxidx), |
595 shyps = union_sort (shypsA, shyps), |
595 shyps = union_sort (shypsA, shyps), |
596 hyps = union_term(hypsA,hyps), (*dups suppressed*) |
596 hyps = union_term(hypsA,hyps), (*dups suppressed*) |
597 prop = B} |
597 prop = B} |
598 else err("major premise") |
598 else err("major premise") |
633 Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => |
633 Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => |
634 if T<>qary then |
634 if T<>qary then |
635 raise THM("forall_elim: type mismatch", 0, [th]) |
635 raise THM("forall_elim: type mismatch", 0, [th]) |
636 else let val thm = fix_shyps [th] [] |
636 else let val thm = fix_shyps [th] [] |
637 (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), |
637 (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), |
638 der = Pt.infer_derivs' (Pt.%% o rpair (Some t)) der, |
638 der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der, |
639 maxidx = Int.max(maxidx, maxt), |
639 maxidx = Int.max(maxidx, maxt), |
640 shyps = [], |
640 shyps = [], |
641 hyps = hyps, |
641 hyps = hyps, |
642 prop = betapply(A,t)}) |
642 prop = betapply(A,t)}) |
643 in if maxt >= 0 andalso maxidx >= 0 |
643 in if maxt >= 0 andalso maxidx >= 0 |