changeset 37254 | da728f9a68e8 |
parent 35387 | 4356263e0bdd |
child 37375 | cf5e06d5ecaf |
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"