| changeset 35387 | 4356263e0bdd |
| parent 35372 | ca158c7b1144 |
| parent 35386 | 45a4e19d3ebd |
| child 37255 | da728f9a68e8 |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 16:50:09 2010 +0100 @@ -64,7 +64,7 @@ oops lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" -nitpick [expect = none] +nitpick [fast_descrs (* ### FIXME *), expect = none] sorry lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"