# HG changeset patch
# User blanchet
# Date 1275468653 -7200
# Node ID 119c2901304c144edc5c4d22fc2abac82962de96
# Parent  12fdf42af8baa4891c77f709ee81f50095a93a15
fix parameter settings

diff -r 12fdf42af8ba -r 119c2901304c src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 20:52:01 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Jun 02 10:50:53 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 [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI,
+                max_threads = 1, timeout = 60 s]
 
 subsection {* Curry in a Hurry *}
 
@@ -1051,52 +1051,56 @@
 nitpick [expect = none]
 sorry
 
+nitpick_params [full_descrs, max_potential = 1]
+
 lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *)
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = potential] (* unfortunate *)
 oops
 
 lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
 sorry
 
 lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
 sorry
 
 lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+nitpick [card nat = 14, expect = genuine]
 oops
 
 lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+nitpick [card nat = 14, expect = genuine]
 oops
 
 lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = genuine]
 oops
 
 lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
 oops
 
 lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
-nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+nitpick [card nat = 4, expect = potential]
+nitpick [card nat = 14, expect = none]
 sorry
 
 lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+nitpick [card nat = 14, expect = genuine]
 oops
 
 lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+nitpick [card nat = 14, expect = none]
 sorry
 
+nitpick_params [fast_descrs, max_potential = 0]
+
 subsection {* Destructors and Recursors *}
 
 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"