equal
deleted
inserted
replaced
716 else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; |
716 else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; |
717 |
717 |
718 (*Called by the oracle-based methods declared in res_atp_methods.ML*) |
718 (*Called by the oracle-based methods declared in res_atp_methods.ML*) |
719 fun write_subgoal_file dfg mode ctxt conjectures user_thms n = |
719 fun write_subgoal_file dfg mode ctxt conjectures user_thms n = |
720 let val conj_cls = make_clauses conjectures |
720 let val conj_cls = make_clauses conjectures |
721 |> ResAxioms.assume_abstract_list true |> Meson.finish_cnf |
721 |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf |
722 val hyp_cls = cnf_hyps_thms ctxt |
722 val hyp_cls = cnf_hyps_thms ctxt |
723 val goal_cls = conj_cls@hyp_cls |
723 val goal_cls = conj_cls@hyp_cls |
724 val goal_tms = map prop_of goal_cls |
724 val goal_tms = map prop_of goal_cls |
725 val thy = ProofContext.theory_of ctxt |
725 val thy = ProofContext.theory_of ctxt |
726 val logic = case mode of |
726 val logic = case mode of |