1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 20:52:01 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Jun 02 10:50:53 2010 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     1.8 -                timeout = 60 s]
     1.9 +nitpick_params [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI,
    1.10 +                max_threads = 1, timeout = 60 s]
    1.11  
    1.12  subsection {* Curry in a Hurry *}
    1.13  
    1.14 @@ -1051,52 +1051,56 @@
    1.15  nitpick [expect = none]
    1.16  sorry
    1.17  
    1.18 +nitpick_params [full_descrs, max_potential = 1]
    1.19 +
    1.20  lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
    1.21 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.22 -nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *)
    1.23 +nitpick [card nat = 4, expect = potential]
    1.24 +nitpick [card nat = 14, expect = potential] (* unfortunate *)
    1.25  oops
    1.26  
    1.27  lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
    1.28 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.29 -nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.30 +nitpick [card nat = 4, expect = potential]
    1.31 +nitpick [card nat = 14, expect = none]
    1.32  sorry
    1.33  
    1.34  lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
    1.35 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.36 -nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.37 +nitpick [card nat = 4, expect = potential]
    1.38 +nitpick [card nat = 14, expect = none]
    1.39  sorry
    1.40  
    1.41  lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
    1.42 -nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.43 +nitpick [card nat = 14, expect = genuine]
    1.44  oops
    1.45  
    1.46  lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
    1.47 -nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.48 +nitpick [card nat = 14, expect = genuine]
    1.49  oops
    1.50  
    1.51  lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
    1.52 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.53 -nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.54 +nitpick [card nat = 4, expect = potential]
    1.55 +nitpick [card nat = 14, expect = genuine]
    1.56  oops
    1.57  
    1.58  lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
    1.59 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.60 -nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.61 +nitpick [card nat = 4, expect = potential]
    1.62 +nitpick [card nat = 14, expect = none]
    1.63  oops
    1.64  
    1.65  lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
    1.66 -nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.67 -nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.68 +nitpick [card nat = 4, expect = potential]
    1.69 +nitpick [card nat = 14, expect = none]
    1.70  sorry
    1.71  
    1.72  lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
    1.73 -nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.74 +nitpick [card nat = 14, expect = genuine]
    1.75  oops
    1.76  
    1.77  lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
    1.78 -nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.79 +nitpick [card nat = 14, expect = none]
    1.80  sorry
    1.81  
    1.82 +nitpick_params [fast_descrs, max_potential = 0]
    1.83 +
    1.84  subsection {* Destructors and Recursors *}
    1.85  
    1.86  lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"