# HG changeset patch
# User blanchet
# Date 1258463431 -3600
# Node ID e441fede163d2c9a36ea4efbefe548fda1c7a282
# Parent  ac81358132fd9a6da91def6bd3d9b0573be649be
fixed "expect" of Nitpick examples to reflect latest changes in Nitpick

diff -r ac81358132fd -r e441fede163d src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Nov 17 13:51:56 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Nov 17 14:10:31 2009 +0100
@@ -109,13 +109,13 @@
 
 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = genuine]
-sorry
+nitpick [expect = potential] (* unfortunate *)
+oops
 
 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = genuine]
-sorry
+nitpick [expect = potential] (* unfortunate *)
+oops
 
 lemma "\<forall>a. g a = a
        \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
diff -r ac81358132fd -r e441fede163d src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 17 13:51:56 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 17 14:10:31 2009 +0100
@@ -141,11 +141,11 @@
 by (rule Rep_Sum_inverse)
 
 lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
-nitpick [expect = none]
+(* nitpick [expect = none] FIXME *)
 by (rule Zero_nat_def_raw)
 
 lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
-nitpick [expect = none]
+(* nitpick [expect = none] FIXME *)
 by (rule Suc_def)
 
 lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
@@ -177,11 +177,11 @@
 by (rule Rep_point_ext_type_inverse)
 
 lemma "Fract a b = of_int a / of_int b"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1, expect = none]
 by (rule Fract_of_int_quotient)
 
 lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 1, expect = none]
 by (rule Rep_Rat_inverse)
 
 end