# HG changeset patch # User blanchet # Date 1301916454 -7200 # Node ID 9e2673711c778166bd1a5aa949ffd4aaf11bfcb7 # Parent 02513eb26eb70da3cb54daa4d960e0b1bcc2062c make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option diff -r 02513eb26eb7 -r 9e2673711c77 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 *}