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.
Slight modification to trace information.
authormengj
Mon, 28 Nov 2005 07:14:12 +0100
changeset 18272 4f0904ba19c2
parent 18271 0e9a851db989
child 18273 e15a825da262
Slight modification to trace information.
src/HOL/Tools/res_atp_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:13:43 2005 +0100
+++ b/src/HOL/Tools/res_atp_provers.ML	Mon Nov 28 07:14:12 2005 +0100
@@ -39,11 +39,11 @@
 
 
 
-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)  
+fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); 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 ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd helper); 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 files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
   else (raise Fail ("eprover oracle failed")));
 
 end;
isabelle