equal
deleted
inserted
replaced
133 |
133 |
134 subsection {* Waldmeister helpers *} |
134 subsection {* Waldmeister helpers *} |
135 |
135 |
136 (* Has all needed simplification lemmas for logic. |
136 (* Has all needed simplification lemmas for logic. |
137 "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *) |
137 "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *) |
138 lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb |
138 lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb |
139 eq_ac disj_comms disj_assoc conj_comms conj_assoc |
139 eq_ac disj_comms disj_assoc conj_comms conj_assoc |
140 |
140 |
141 |
141 |
142 subsection {* Basic connection between ATPs and HOL *} |
142 subsection {* Basic connection between ATPs and HOL *} |
143 |
143 |