equal
deleted
inserted
replaced
552 val tracing = ref false; |
552 val tracing = ref false; |
553 |
553 |
554 fun say s = if !tracing then writeln s else (); |
554 fun say s = if !tracing then writeln s else (); |
555 |
555 |
556 fun print_thms s L = |
556 fun print_thms s L = |
557 say (cat_lines (s :: map string_of_thm L)); |
557 say (cat_lines (s :: map Display.string_of_thm L)); |
558 |
558 |
559 fun print_cterms s L = |
559 fun print_cterms s L = |
560 say (cat_lines (s :: map string_of_cterm L)); |
560 say (cat_lines (s :: map Display.string_of_cterm L)); |
561 |
561 |
562 |
562 |
563 (*--------------------------------------------------------------------------- |
563 (*--------------------------------------------------------------------------- |
564 * General abstraction handlers, should probably go in USyntax. |
564 * General abstraction handlers, should probably go in USyntax. |
565 *---------------------------------------------------------------------------*) |
565 *---------------------------------------------------------------------------*) |
677 let fun cong_prover ss thm = |
677 let fun cong_prover ss thm = |
678 let val dummy = say "cong_prover:" |
678 let val dummy = say "cong_prover:" |
679 val cntxt = MetaSimplifier.prems_of_ss ss |
679 val cntxt = MetaSimplifier.prems_of_ss ss |
680 val dummy = print_thms "cntxt:" cntxt |
680 val dummy = print_thms "cntxt:" cntxt |
681 val dummy = say "cong rule:" |
681 val dummy = say "cong rule:" |
682 val dummy = say (string_of_thm thm) |
682 val dummy = say (Display.string_of_thm thm) |
683 val dummy = thm_ref := (thm :: !thm_ref) |
683 val dummy = thm_ref := (thm :: !thm_ref) |
684 val dummy = ss_ref := (ss :: !ss_ref) |
684 val dummy = ss_ref := (ss :: !ss_ref) |
685 (* Unquantified eliminate *) |
685 (* Unquantified eliminate *) |
686 fun uq_eliminate (thm,imp,thy) = |
686 fun uq_eliminate (thm,imp,thy) = |
687 let val tych = cterm_of thy |
687 let val tych = cterm_of thy |