accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)
authorhaftmann
Fri, 02 Jul 2010 16:10:59 +0200
changeset 376871a6f475085fc
parent 37686 71e84a203c19
child 37688 db7b5f2e19cd
accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)
src/HOL/Nitpick_Examples/Datatype_Nits.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Jul 02 14:23:18 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Jul 02 16:10:59 2010 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  oops
     1.5  
     1.6  lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
     1.7 -nitpick [card = 1\<midarrow>9, expect = none]
     1.8 +nitpick [card = 1\<midarrow>9, expect = unknown (*none*)]
     1.9  sorry
    1.10  
    1.11  lemma "fs (Pd ((a, b), (c, d))) = (c, d)"