equal
deleted
inserted
replaced
574 |
574 |
575 (**** prover-specific format: TPTP ****) |
575 (**** prover-specific format: TPTP ****) |
576 |
576 |
577 |
577 |
578 fun cnf_hyps_thms ctxt = |
578 fun cnf_hyps_thms ctxt = |
579 let val ths = ProofContext.prems_of ctxt |
579 let val ths = Assumption.prems_of ctxt |
580 in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; |
580 in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; |
581 |
581 |
582 |
582 |
583 (**** write to files ****) |
583 (**** write to files ****) |
584 |
584 |