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.
compile
authorblanchet
Wed, 24 Feb 2010 11:55:52 +0100
changeset 35342 4dc65845eab3
parent 35341 c6bbfa9c4eca
child 35350 0df9c8a37f64
child 35416 d8d7d1b785af
compile
src/HOL/Nitpick_Examples/Refute_Nits.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:35:39 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 11:55:52 2010 +0100
@@ -1430,12 +1430,6 @@
 apply intro_classes
 done
 
-lemma "OFCLASS('a, classB_class)"
-nitpick [expect = none]
-apply intro_classes
-apply simp
-done
-
 lemma "OFCLASS('a\<Colon>type, classC_class)"
 nitpick [expect = genuine]
 oops
isabelle