diff -r c3c7a09a3ada -r 539cc471186f src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Sat Sep 20 10:44:23 2014 +0200
+++ b/src/HOL/ATP.thy	Sat Sep 20 10:44:24 2014 +0200
@@ -133,10 +133,15 @@
 
 subsection {* Waldmeister helpers *}
 
-(* Has all needed simplification lemmas for logic.
-   "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
-lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
-  eq_ac disj_comms disj_assoc conj_comms conj_assoc
+(* Has all needed simplification lemmas for logic. *)
+lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
+  by simp
+
+lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)"
+  by metis
+
+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
 
 
 subsection {* Basic connection between ATPs and HOL *}
@@ -148,6 +153,6 @@
 ML_file "Tools/ATP/atp_systems.ML"
 ML_file "Tools/ATP/atp_waldmeister.ML"
 
-hide_fact (open) waldmeister_fol
+hide_fact (open) waldmeister_fol boolean_equality boolean_comm
 
 end