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.
revert unintended "sledgehammer" call
authorblanchet
Mon, 09 Jan 2012 18:32:56 +0100
changeset 46162 1148fab5104e
parent 46118 e99ca055c91d
child 46163 6c880b26dfc4
revert unintended "sledgehammer" call
src/HOL/Nitpick_Examples/Manual_Nits.thy file | annotate | diff | comparison | revisions 
--- 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 *}
isabelle