src/HOL/Nitpick_Examples/Special_Nits.thy
changeset 33737 e441fede163d
parent 33197 de6285ebcc05
child 34083 652719832159
     1.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Nov 17 13:51:56 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Nov 17 14:10:31 2009 +0100
     1.3 @@ -109,13 +109,13 @@
     1.4  
     1.5  lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
     1.6         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
     1.7 -nitpick [expect = genuine]
     1.8 -sorry
     1.9 +nitpick [expect = potential] (* unfortunate *)
    1.10 +oops
    1.11  
    1.12  lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
    1.13         f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
    1.14 -nitpick [expect = genuine]
    1.15 -sorry
    1.16 +nitpick [expect = potential] (* unfortunate *)
    1.17 +oops
    1.18  
    1.19  lemma "\<forall>a. g a = a
    1.20         \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =