exported linkup_logic_mode and changed the default setting
authorpaulson
Wed Apr 19 13:11:35 2006 +0200 (2006-04-19 ago)
changeset 19450651d949776f8
parent 19449 b07e3bca20c9
child 19451 c7a25c05986c
exported linkup_logic_mode and changed the default setting
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Apr 19 10:43:53 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Apr 19 13:11:35 2006 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val time_limit: int ref
     1.5     
     1.6    datatype mode = Auto | Fol | Hol
     1.7 +  val linkup_logic_mode : mode ref
     1.8    val write_subgoal_file: mode -> Proof.context -> thm list -> thm list -> int -> string
     1.9    val vampire_time: int ref
    1.10    val eprover_time: int ref
    1.11 @@ -339,7 +340,7 @@
    1.12  
    1.13  datatype mode = Auto | Fol | Hol;
    1.14  
    1.15 -val linkup_logic_mode = ref Fol;
    1.16 +val linkup_logic_mode = ref Auto;
    1.17  
    1.18  fun tptp_writer logic goals filename (axioms,classrels,arities) =
    1.19      if is_fol_logic logic