src/HOL/Nitpick_Examples/Refute_Nits.thy
changeset 38185 b51677438b3a
parent 36319 8feb2c4bef1a
child 40341 03156257040f
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
@@ -11,8 +11,8 @@
 imports Main
 begin
 
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6, max_potential = 0,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 lemma "P \<and> Q"
 apply (rule conjI)