--- 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