author blanchet Fri Oct 23 20:13:33 2009 +0200 (2009-10-23) changeset 33199 6c9b2a94a69c parent 33198 bfb9a790d1e7 child 33200 c56c627dae19
make the Nitpick examples work again
1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
1.3 @@ -714,7 +714,7 @@
1.5  lemma "{} = (\<lambda>x. False)"
1.6  nitpick [expect = none]
1.7 -by (metis Collect_def bot_set_eq empty_def)
1.8 +by (metis Collect_def empty_def)
1.10  lemma "x \<in> {}"
1.11  nitpick [expect = genuine]
2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
2.3 @@ -40,15 +40,15 @@
2.4  nitpick [card = 2, max Nibble3 = 0, expect = none]
2.5  oops
2.7 -lemma "fun_pow 15 rot n \<noteq> n"
2.8 +lemma "(rot ^^ 15) n \<noteq> n"
2.9  nitpick [card = 17, expect = none]
2.10  sorry
2.12 -lemma "fun_pow 15 rot n = n"
2.13 +lemma "(rot ^^ 15) n = n"
2.14  nitpick [card = 17, expect = genuine]
2.15  oops
2.17 -lemma "fun_pow 16 rot n = n"
2.18 +lemma "(rot ^^ 16) n = n"
2.19  nitpick [card = 17, expect = none]
2.20  oops
3.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
3.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
3.3 @@ -157,11 +157,11 @@
3.4  by (rule Rep_Nat_inverse)
3.6  lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
3.7 -nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = unknown]
3.8 +nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
3.9  by (rule Zero_int_def_raw)
3.11  lemma "Abs_Integ (Rep_Integ a) = a"
3.12 -nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = none]
3.13 +nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
3.14  by (rule Rep_Integ_inverse)
3.16  lemma "Abs_list (Rep_list a) = a"
3.17 @@ -173,15 +173,15 @@
3.18    Ycoord :: int
3.20  lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
3.21 -nitpick [expect = none]
3.22 +nitpick [expect = unknown]
3.23  by (rule Rep_point_ext_type_inverse)
3.25  lemma "Fract a b = of_int a / of_int b"
3.26 -nitpick [card = 1\<midarrow>2, expect = potential]
3.27 +nitpick [card = 1\<midarrow>2, expect = unknown]
3.28  by (rule Fract_of_int_quotient)
3.30  lemma "Abs_Rat (Rep_Rat a) = a"
3.31 -nitpick [card = 1\<midarrow>2, expect = none]
3.32 +nitpick [card = 1\<midarrow>2, expect = unknown]
3.33  by (rule Rep_Rat_inverse)
3.35  end