author | paulson |

Thu Jun 14 13:19:50 2007 +0200 (2007-06-14) | |

changeset 23387 | 7cb8faa5d4d3 |

parent 23386 | 9255c1a75ba9 |

child 23388 | 77645da0db85 |

Now ResHolClause also does first-order problems!

1.1 --- a/src/HOL/Tools/res_atp.ML Thu Jun 14 13:18:59 2007 +0200 1.2 +++ b/src/HOL/Tools/res_atp.ML Thu Jun 14 13:19:50 2007 +0200 1.3 @@ -691,15 +691,9 @@ 1.4 likely to lead to unsound proofs.*) 1.5 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; 1.6 1.7 -fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas = 1.8 - if is_fol_logic logic 1.9 - then ResClause.tptp_write_file goals filename (axioms, classrels, arities) 1.10 - else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas; 1.11 +fun tptp_writer logic = ResHolClause.tptp_write_file (logic=FOL); 1.12 1.13 -fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas = 1.14 - if is_fol_logic logic 1.15 - then ResClause.dfg_write_file goals filename (axioms, classrels, arities) 1.16 - else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; 1.17 +fun dfg_writer logic = ResHolClause.dfg_write_file (logic=FOL); 1.18 1.19 (*Called by the oracle-based methods declared in res_atp_methods.ML*) 1.20 fun write_subgoal_file dfg mode ctxt conjectures user_thms n = 1.21 @@ -819,7 +813,7 @@ 1.22 get_neg_subgoals gls (n+1) 1.23 val goal_cls = get_neg_subgoals goals 1 1.24 val logic = case !linkup_logic_mode of 1.25 - Auto => problem_logic_goals (map ((map prop_of)) goal_cls) 1.26 + Auto => problem_logic_goals (map (map prop_of) goal_cls) 1.27 | Fol => FOL 1.28 | Hol => HOL 1.29 val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []