Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
authormengj
Fri, 18 Nov 2005 07:07:06 +0100
changeset 18196 02f1c4022484
parent 18195 971dc7439088
child 18197 082a2bd6f655
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
src/HOL/Tools/res_atp_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:06:07 2005 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Fri Nov 18 07:07:06 2005 +0100
@@ -39,11 +39,11 @@
 
 
 
-fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
+fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
   else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
 
 
-fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
+fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
   else (raise Fail ("eprover oracle failed")));
 
 end;
isabelle