src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 40698 8a3f7ea91370
parent 40693 a4171afcc3c4
child 40701 e7aa34600c36
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 14:58:20 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 14:58:50 2010 +0100
@@ -104,8 +104,9 @@
     else is_atp_installed thy name
   end
 
-val smt_default_max_relevant = 200 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+(* FUDGE *)
+val smt_default_max_relevant = 200
+val auto_max_relevant_divisor = 2
 
 fun default_max_relevant_for_prover thy name =
   if is_smt_prover name then smt_default_max_relevant
@@ -432,6 +433,7 @@
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
+(* FUDGE *)
 val smt_max_iter = 8
 val smt_iter_fact_divisor = 2
 val smt_iter_min_msecs = 5000