Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
obsolete FIXME
authorblanchet
Mon, 31 May 2010 18:51:06 +0200
changeset 37255 da728f9a68e8
parent 37254 3625d37a0079
child 37256 0dca1ec52999
obsolete FIXME
src/HOL/Nitpick_Examples/Typedef_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon May 31 18:49:32 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon May 31 18:51:06 2010 +0200
@@ -64,7 +64,7 @@
 oops
 
 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [fast_descrs (* ### FIXME *), expect = none]
+nitpick [expect = none]
 sorry
 
 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
isabelle