src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 34126 8a2c5d7aff51
parent 34083 652719832159
child 35076 cc19e2aef17e
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -876,7 +876,7 @@
     1.4  by auto
     1.5  
     1.6  lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
     1.7 -nitpick [expect = none]
     1.8 +nitpick [card = 1\<midarrow>7, expect = none]
     1.9  by auto
    1.10  
    1.11  lemma "A \<union> - A = UNIV"
    1.12 @@ -892,7 +892,7 @@
    1.13  oops
    1.14  
    1.15  lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
    1.16 -nitpick [expect = none]
    1.17 +nitpick [card = 1\<midarrow>7, expect = none]
    1.18  oops
    1.19  
    1.20  lemma "finite A"