specify proper defaults for Nitpick and Refute on TPTP + tuning
authorblanchet
Thu Mar 24 17:49:27 2011 +0100 (2011-03-24)
changeset 42106ed1d40888b1b
parent 42105 bba85afcfedf
child 42107 a6725f293377
specify proper defaults for Nitpick and Refute on TPTP + tuning
src/HOL/ex/TPTP.thy
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/ex/TPTP.thy	Thu Mar 24 17:49:27 2011 +0100
     1.2 +++ b/src/HOL/ex/TPTP.thy	Thu Mar 24 17:49:27 2011 +0100
     1.3 @@ -14,6 +14,10 @@
     1.4  
     1.5  declare [[smt_oracle]]
     1.6  
     1.7 +refute_params [maxtime = 10000, no_assms, expect = genuine]
     1.8 +nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
     1.9 +                expect = genuine]
    1.10 +
    1.11  ML {* Proofterm.proofs := 0 *}
    1.12  
    1.13  ML {*
     2.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Mar 24 17:49:27 2011 +0100
     2.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Mar 24 17:49:27 2011 +0100
     2.3 @@ -50,11 +50,6 @@
     2.4        handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
     2.5    end
     2.6  
     2.7 -fun to_period ("." :: _) = []
     2.8 -  | to_period ("" :: ss) = to_period ss
     2.9 -  | to_period (s :: ss) = s :: to_period ss
    2.10 -  | to_period [] = []
    2.11 -
    2.12  val atp = "e" (* or "vampire" or "spass" etc. *)
    2.13  
    2.14  fun thms_of_name ctxt name =