equal
deleted
inserted
replaced
655 val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref |
655 val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref |
656 val cut_lemma' = cut_lemma RS eq_reflection |
656 val cut_lemma' = cut_lemma RS eq_reflection |
657 fun prover used ss thm = |
657 fun prover used ss thm = |
658 let fun cong_prover ss thm = |
658 let fun cong_prover ss thm = |
659 let val dummy = say "cong_prover:" |
659 let val dummy = say "cong_prover:" |
660 val cntxt = Simplifier.prems_of_ss ss |
660 val cntxt = Simplifier.prems_of ss |
661 val dummy = print_thms "cntxt:" cntxt |
661 val dummy = print_thms "cntxt:" cntxt |
662 val dummy = say "cong rule:" |
662 val dummy = say "cong rule:" |
663 val dummy = say (Display.string_of_thm_without_context thm) |
663 val dummy = say (Display.string_of_thm_without_context thm) |
664 (* Unquantified eliminate *) |
664 (* Unquantified eliminate *) |
665 fun uq_eliminate (thm,imp,thy) = |
665 fun uq_eliminate (thm,imp,thy) = |
737 in SOME(eliminate (rename thm)) end |
737 in SOME(eliminate (rename thm)) end |
738 handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) |
738 handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) |
739 |
739 |
740 fun restrict_prover ss thm = |
740 fun restrict_prover ss thm = |
741 let val dummy = say "restrict_prover:" |
741 let val dummy = say "restrict_prover:" |
742 val cntxt = rev(Simplifier.prems_of_ss ss) |
742 val cntxt = rev (Simplifier.prems_of ss) |
743 val dummy = print_thms "cntxt:" cntxt |
743 val dummy = print_thms "cntxt:" cntxt |
744 val thy = Thm.theory_of_thm thm |
744 val thy = Thm.theory_of_thm thm |
745 val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm |
745 val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm |
746 fun genl tm = let val vlist = subtract (op aconv) globals |
746 fun genl tm = let val vlist = subtract (op aconv) globals |
747 (OldTerm.add_term_frees(tm,[])) |
747 (OldTerm.add_term_frees(tm,[])) |