src/HOL/ATP.thy
changeset 58407 111d801b5d5d
parent 58406 539cc471186f
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4    by simp
     1.5  
     1.6  lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
     1.7 -  by metis
     1.8 +  by auto
     1.9  
    1.10  lemmas waldmeister_fol = boolean_equality boolean_comm
    1.11    simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc