crank up limit a bit -- truly huge background theories are still nearly 3 times larger
authorblanchet
Wed Oct 09 08:12:53 2013 +0200 (2013-10-09 ago)
changeset 54083824db6ab3339
parent 54082 fcb7bbbe3799
child 54084 c2782ec22cc6
crank up limit a bit -- truly huge background theories are still nearly 3 times larger
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 22:33:05 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 08:12:53 2013 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  val max_facts_for_duplicates = 50000
     1.5  val max_facts_for_duplicate_matching = 25000
     1.6  val max_facts_for_complex_check = 25000
     1.7 -val max_simps_for_clasimpset = 5000
     1.8 +val max_simps_for_clasimpset = 10000
     1.9  
    1.10  (* experimental feature *)
    1.11  val instantiate_inducts =