obsolete FIXME
authorblanchet
Mon, 31 May 2010 18:51:06 +0200
changeset 37254da728f9a68e8
parent 37253 3625d37a0079
child 37255 0dca1ec52999
obsolete FIXME
src/HOL/Nitpick_Examples/Typedef_Nits.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon May 31 18:49:32 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon May 31 18:51:06 2010 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  oops
     1.5  
     1.6  lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
     1.7 -nitpick [fast_descrs (* ### FIXME *), expect = none]
     1.8 +nitpick [expect = none]
     1.9  sorry
    1.10  
    1.11  lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"