--- 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)"