--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Oct 23 19:00:36 2009 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Oct 23 20:13:33 2009 +0200
@@ -714,7 +714,7 @@
lemma "{} = (\<lambda>x. False)"
nitpick [expect = none]
-by (metis Collect_def bot_set_eq empty_def)
+by (metis Collect_def empty_def)
lemma "x \<in> {}"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Oct 23 19:00:36 2009 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Oct 23 20:13:33 2009 +0200
@@ -40,15 +40,15 @@
nitpick [card = 2, max Nibble3 = 0, expect = none]
oops
-lemma "fun_pow 15 rot n \<noteq> n"
+lemma "(rot ^^ 15) n \<noteq> n"
nitpick [card = 17, expect = none]
sorry
-lemma "fun_pow 15 rot n = n"
+lemma "(rot ^^ 15) n = n"
nitpick [card = 17, expect = genuine]
oops
-lemma "fun_pow 16 rot n = n"
+lemma "(rot ^^ 16) n = n"
nitpick [card = 17, expect = none]
oops
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 23 19:00:36 2009 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 23 20:13:33 2009 +0200
@@ -157,11 +157,11 @@
by (rule Rep_Nat_inverse)
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = unknown]
+nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
by (rule Zero_int_def_raw)
lemma "Abs_Integ (Rep_Integ a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = none]
+nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
by (rule Rep_Integ_inverse)
lemma "Abs_list (Rep_list a) = a"
@@ -173,15 +173,15 @@
Ycoord :: int
lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
-nitpick [expect = none]
+nitpick [expect = unknown]
by (rule Rep_point_ext_type_inverse)
lemma "Fract a b = of_int a / of_int b"
-nitpick [card = 1\<midarrow>2, expect = potential]
+nitpick [card = 1\<midarrow>2, expect = unknown]
by (rule Fract_of_int_quotient)
lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1\<midarrow>2, expect = unknown]
by (rule Rep_Rat_inverse)
end