--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Nov 06 10:25:08 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Nov 06 10:25:08 2010 +0100
@@ -23,7 +23,7 @@
"rot NibbleF = Nibble0"
lemma "rot n \<noteq> n"
-nitpick [card = 1\<midarrow>16, expect = none]
+nitpick [card = 1\<midarrow>8,16, verbose, expect = none]
sorry
lemma "rot Nibble2 \<noteq> Nibble3"
@@ -69,7 +69,7 @@
oops
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
-nitpick [card = 1\<midarrow>9, expect = none]
+nitpick [expect = none]
sorry
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
@@ -82,7 +82,7 @@
"app (Fn f) x = f x"
lemma "app (Fn g) y = g y"
-nitpick [card = 1\<midarrow>10, expect = none]
+nitpick [expect = none]
sorry
lemma "app (Fn g) y = g' y"