--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
subsection {* Curry in a Hurry *}
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
@@ -135,7 +137,7 @@
by (auto simp: Id_def Collect_def)
lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
-nitpick [card = 1\<midarrow>20, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
by (auto simp: Id_def Collect_def)
lemma "UNIV (x\<Colon>'a\<times>'a)"
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
primrec rot where
"rot Nibble0 = Nibble1" |
"rot Nibble1 = Nibble2" |
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [show_all]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [card = 14]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+ card = 14]
lemma "x = (case u of () \<Rightarrow> y)"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
record point2d =
xc :: int
yc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+
lemma "P \<and> Q"
apply (rule conjI)
nitpick [expect = genuine] 1
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [card = 4, debug, show_consts, timeout = 10 s]
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+ card = 4]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
"f1 a b c d e = a + b + c + d + e"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Dec 14 10:24:04 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Dec 14 11:01:04 2009 +0100
@@ -137,7 +137,7 @@
by (rule Inl_Rep_not_Inr_Rep)
lemma "Abs_Sum (Rep_Sum a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
@@ -157,15 +157,15 @@
by (rule Rep_Nat_inverse)
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
+nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
by (rule Zero_int_def_raw)
lemma "Abs_Integ (Rep_Integ a) = a"
-nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
+nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
by (rule Rep_Integ_inverse)
lemma "Abs_list (Rep_list a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
by (rule Rep_list_inverse)
record point =