--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Oct 29 15:23:25 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Oct 29 15:24:52 2009 +0100
@@ -173,15 +173,15 @@
Ycoord :: int
lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
-nitpick [expect = unknown]
+nitpick [expect = none]
by (rule Rep_point_ext_type_inverse)
lemma "Fract a b = of_int a / of_int b"
-nitpick [card = 1\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Fract_of_int_quotient)
lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Rep_Rat_inverse)
end