diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 12:14:29 2010 +0100 @@ -149,7 +149,7 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" -nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *) +nitpick [card nat = 10, unary_ints, verbose, show_consts] oops lemma "even' (n - 2) \ even' n"