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.
exported linkup_logic_mode and changed the default setting
authorpaulson
Wed, 19 Apr 2006 13:11:35 +0200
changeset 19450 651d949776f8
parent 19449 b07e3bca20c9
child 19451 c7a25c05986c
exported linkup_logic_mode and changed the default setting
src/HOL/Tools/res_atp.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_atp.ML	Wed Apr 19 10:43:53 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Apr 19 13:11:35 2006 +0200
@@ -15,6 +15,7 @@
   val time_limit: int ref
    
   datatype mode = Auto | Fol | Hol
+  val linkup_logic_mode : mode ref
   val write_subgoal_file: mode -> Proof.context -> thm list -> thm list -> int -> string
   val vampire_time: int ref
   val eprover_time: int ref
@@ -339,7 +340,7 @@
 
 datatype mode = Auto | Fol | Hol;
 
-val linkup_logic_mode = ref Fol;
+val linkup_logic_mode = ref Auto;
 
 fun tptp_writer logic goals filename (axioms,classrels,arities) =
     if is_fol_logic logic
isabelle