1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Thu Dec 05 13:22:00 2013 +0100
1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Thu Dec 05 13:38:20 2013 +0100
1.3 @@ -12,7 +12,7 @@
1.4 begin
1.5
1.6 nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0,
1.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
1.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
1.9
1.10 subsection {* Curry in a Hurry *}
1.11
2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Dec 05 13:22:00 2013 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Dec 05 13:38:20 2013 +0100
2.3 @@ -12,7 +12,7 @@
2.4 begin
2.5
2.6 nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0,
2.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
2.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
2.9
2.10 primrec rot where
2.11 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
3.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Thu Dec 05 13:22:00 2013 +0100
3.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Thu Dec 05 13:38:20 2013 +0100
3.3 @@ -12,7 +12,7 @@
3.4 imports Main
3.5 begin
3.6
3.7 -nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
3.8 +nitpick_params [verbose, max_potential = 0, sat_solver = Riss3g,
3.9 max_threads = 1, timeout = 240]
3.10
3.11 typedecl guest
4.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Thu Dec 05 13:22:00 2013 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Thu Dec 05 13:38:20 2013 +0100
4.3 @@ -12,7 +12,7 @@
4.4 begin
4.5
4.6 nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
4.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
4.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
4.9
4.10 inductive p1 :: "nat \<Rightarrow> bool" where
4.11 "p1 0" |
5.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Dec 05 13:22:00 2013 +0100
5.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Dec 05 13:38:20 2013 +0100
5.3 @@ -12,7 +12,7 @@
5.4 begin
5.5
5.6 nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
5.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
5.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
5.9
5.10 lemma "Suc x = x + 1"
5.11 nitpick [unary_ints, expect = none]
6.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Dec 05 13:22:00 2013 +0100
6.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Dec 05 13:38:20 2013 +0100
6.3 @@ -17,7 +17,7 @@
6.4
6.5 chapter {* 2. First Steps *}
6.6
6.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
6.8 +nitpick_params [sat_solver = Riss3g, max_threads = 1, timeout = 240]
6.9
6.10 subsection {* 2.1. Propositional Logic *}
6.11
7.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Dec 05 13:22:00 2013 +0100
7.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Dec 05 13:38:20 2013 +0100
7.3 @@ -13,7 +13,7 @@
7.4
7.5 ML_file "minipick.ML"
7.6
7.7 -nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
7.8 +nitpick_params [verbose, sat_solver = Riss3g, max_threads = 1]
7.9
7.10 nitpick_params [total_consts = smart]
7.11
8.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Thu Dec 05 13:22:00 2013 +0100
8.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Thu Dec 05 13:38:20 2013 +0100
8.3 @@ -11,7 +11,7 @@
8.4 imports Main
8.5 begin
8.6
8.7 -nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat_JNI,
8.8 +nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = Riss3g,
8.9 max_threads = 1, timeout = 240]
8.10
8.11 lemma "x = (case u of () \<Rightarrow> y)"
9.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Thu Dec 05 13:22:00 2013 +0100
9.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Thu Dec 05 13:38:20 2013 +0100
9.3 @@ -12,7 +12,7 @@
9.4 begin
9.5
9.6 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
9.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
9.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
9.9
9.10 record point2d =
9.11 xc :: int
10.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Thu Dec 05 13:22:00 2013 +0100
10.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Thu Dec 05 13:38:20 2013 +0100
10.3 @@ -12,7 +12,7 @@
10.4 begin
10.5
10.6 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
10.7 - sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
10.8 + sat_solver = Riss3g, max_threads = 1, timeout = 240]
10.9
10.10 lemma "P \<and> Q"
10.11 apply (rule conjI)
11.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 05 13:22:00 2013 +0100
11.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 05 13:38:20 2013 +0100
11.3 @@ -11,7 +11,7 @@
11.4 imports Main
11.5 begin
11.6
11.7 -nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
11.8 +nitpick_params [verbose, card = 4, sat_solver = Riss3g, max_threads = 1,
11.9 timeout = 240]
11.10
11.11 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
12.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Dec 05 13:22:00 2013 +0100
12.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Dec 05 13:38:20 2013 +0100
12.3 @@ -11,7 +11,7 @@
12.4 imports Complex_Main
12.5 begin
12.6
12.7 -nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
12.8 +nitpick_params [verbose, card = 1\<emdash>4, sat_solver = Riss3g, max_threads = 1,
12.9 timeout = 240]
12.10
12.11 definition "three = {0\<Colon>nat, 1, 2}"