| changeset 35340 | c32d7269bad1 |
| parent 35338 | 38848da259c0 |
| child 35342 | 4dc65845eab3 |
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 24 11:07:58 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 24 11:35:10 2010 +0100 @@ -1418,10 +1418,6 @@ nitpick [expect = genuine] oops -lemma "P (x\<Colon>'a\<Colon>{classB, classE})" -nitpick [expect = genuine] -oops - text {* OFCLASS: *} lemma "OFCLASS('a\<Colon>type, type_class)"