src/HOL/Nitpick_Examples/Manual_Nits.thy
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 *}