--- 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 *}
--- 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" |
--- 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
--- 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" |
--- 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]
--- 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
--- 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)