| changeset 46105 | 9abb756352a6 |
| parent 46104 | eb85282db54e |
| child 46106 | 73e2c70980df |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Jan 03 18:33:18 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Jan 03 23:03:49 2012 +0100 @@ -187,7 +187,7 @@ "\<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 *}