# HG changeset patch # User blanchet # Date 1267008952 -3600 # Node ID 4dc65845eab3f426e7816a7807a1f55845387eaf # Parent c6bbfa9c4eca6b17f2b4f69be5bbca25a7585eda compile diff -r c6bbfa9c4eca -r 4dc65845eab3 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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\type, classC_class)" nitpick [expect = genuine] oops