| changeset 46162 | 1148fab5104e |
| parent 46106 | 73e2c70980df |
| child 47092 | fa3538d6004b |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Jan 05 10:59:18 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Jan 09 18:32:56 2012 +0100 @@ -45,7 +45,6 @@ nitpick [expect = none] nitpick [card 'a = 1\<emdash>50, expect = none] (* sledgehammer *) -sledgehammer by (metis the_equality) subsection {* 2.4. Skolemization *}