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.
Changed proof method to auto for custom Waldmeister lemma
authorsteckerm
Sat, 20 Sep 2014 10:44:24 +0200
changeset 58407 111d801b5d5d
parent 58406 539cc471186f
child 58408 bd5e49fca1fd
Changed proof method to auto for custom Waldmeister lemma
src/HOL/ATP.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
+++ b/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
@@ -138,7 +138,7 @@
   by simp
 
 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
-  by metis
+  by auto
 
 lemmas waldmeister_fol = boolean_equality boolean_comm
   simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
isabelle