diff -r 2a1953f0d20d -r db5026631799 src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Mar 25 20:15:39 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Mon Mar 26 10:42:06 2012 +0200 @@ -198,18 +198,7 @@ lemma "-5 * 55 > (-260::int)" nitpick [unary_ints, expect = none] nitpick [binary_ints, expect = none] -(* BROKEN -Nitpicking formula... -Trying 5 scopes: - card bin = 1, card int = 1, and bits = 9; - card bin = 2, card int = 2, and bits = 9; - card bin = 3, card int = 3, and bits = 9; - card bin = 4, card int = 4, and bits = 9; - card bin = 5, card int = 5, and bits = 9. -Nitpick found no counterexample. -*** Unexpected outcome: "none". nitpick [binary_ints, bits = 9, expect = genuine] -*) oops lemma "nat (of_nat n) = n"