Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ATP.thy
changeset 58407 111d801b5d5d
parent 58406 539cc471186f
child 58889 5b7a9633cfa8 
--- 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