make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
authorblanchet
Mon, 04 Apr 2011 13:27:34 +0200
changeset 42211 9e2673711c77
parent 42208 02513eb26eb7
child 42212 b33d871675bb
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
src/HOL/ex/TPTP.thy
--- a/src/HOL/ex/TPTP.thy	Mon Apr 04 09:32:50 2011 +0200
+++ b/src/HOL/ex/TPTP.thy	Mon Apr 04 13:27:34 2011 +0200
@@ -16,7 +16,7 @@
 
 refute_params [maxtime = 10000, no_assms, expect = genuine]
 nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
-                expect = genuine]
+                batch_size = 1, expect = genuine]
 
 ML {* Proofterm.proofs := 0 *}