# HG changeset patch
# User blanchet
# Date 1256321613 -7200
# Node ID 6c9b2a94a69c147f0bf9f01958bd86ae9b5e67ca
# Parent  bfb9a790d1e7783ee8895fef3cdd1800c51b8ada
make the Nitpick examples work again

diff -r bfb9a790d1e7 -r 6c9b2a94a69c src/HOL/Nitpick_Examples/Core_Nits.thy
--- 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]
diff -r bfb9a790d1e7 -r 6c9b2a94a69c src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- 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
 
diff -r bfb9a790d1e7 -r 6c9b2a94a69c src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- 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