# HG changeset patch
# User blanchet
# Date 1280850195 -7200
# Node ID b51677438b3aa66936f913675fab6b822f9f89c4
# Parent  6a221fffbc8a7dcf5f83a1010b1ff32d0d5be85e
speed up Nitpick examples a little bit

diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
@@ -11,8 +11,8 @@
 imports Main
 begin
 
-nitpick_params [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 subsection {* Curry in a Hurry *}
 
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_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>8, max_potential = 0,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 primrec rot where
 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
@@ -52,7 +52,7 @@
 theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
 nitpick [card room = 1, card guest = 2, card "guest option" = 3,
          card key = 4, card state = 6, expect = genuine]
-nitpick [card room = 1, card guest = 2, expect = genuine]
+(* nitpick [card room = 1, card guest = 2, expect = genuine] *)
 oops
 
 end
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
@@ -11,7 +11,8 @@
 imports Main
 begin
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [card = 1\<midarrow>6,  bits = 1,2,3,4,6,8,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
@@ -11,8 +11,8 @@
 imports Nitpick
 begin
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
-                card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
+nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
 
 lemma "Suc x = x + 1"
 nitpick [unary_ints, expect = none]
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue Aug 03 17:29:54 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Record_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]
 
 record point2d =
   xc :: int
diff -r 6a221fffbc8a -r b51677438b3a src/HOL/Nitpick_Examples/Refute_Nits.thy
--- 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)