src/HOL/Nitpick_Examples/Manual_Nits.thy

 inductive odd where
 "odd 1" |
 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
 
 lemma "odd n \<Longrightarrow> odd (n - 2)"
-nitpick [card nat = 10, show_consts, expect = genuine]
+nitpick [card nat = 4, show_consts, expect = genuine]
 oops
 
 subsection {* 2.9. Coinductive Datatypes *}
 
 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since