
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"




