equal
deleted
inserted
replaced
136 (* Has all needed simplification lemmas for logic. *) |
136 (* Has all needed simplification lemmas for logic. *) |
137 lemma boolean_equality: "(P \<longleftrightarrow> P) = True" |
137 lemma boolean_equality: "(P \<longleftrightarrow> P) = True" |
138 by simp |
138 by simp |
139 |
139 |
140 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)" |
140 lemma boolean_comm: "(P \<longleftrightarrow> Q) = (Q \<longleftrightarrow> P)" |
141 by metis |
141 by auto |
142 |
142 |
143 lemmas waldmeister_fol = boolean_equality boolean_comm |
143 lemmas waldmeister_fol = boolean_equality boolean_comm |
144 simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc |
144 simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc |
145 |
145 |
146 |
146 |