1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  nitpick
     1.5  oops
     1.6  
     1.7 -subsection {* 3.5. Numbers *}
     1.8 +subsection {* 3.5. Natural Numbers and Integers *}
     1.9  
    1.10  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    1.11  nitpick
    1.12 @@ -121,11 +121,11 @@
    1.13  "even n \<Longrightarrow> even (Suc (Suc n))"
    1.14  
    1.15  lemma "\<exists>n. even n \<and> even (Suc n)"
    1.16 -nitpick [card nat = 100, verbose]
    1.17 +nitpick [card nat = 100, unary_ints, verbose]
    1.18  oops
    1.19  
    1.20  lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
    1.21 -nitpick [card nat = 100]
    1.22 +nitpick [card nat = 100, unary_ints, verbose]
    1.23  oops
    1.24  
    1.25  inductive even' where
    1.26 @@ -134,7 +134,7 @@
    1.27  "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
    1.28  
    1.29  lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
    1.30 -nitpick [card nat = 10, verbose, show_consts]
    1.31 +nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
    1.32  oops
    1.33  
    1.34  lemma "even' (n - 2) \<Longrightarrow> even' n"