src/HOL/ATP.thy
changeset 58407 111d801b5d5d
parent 58406 539cc471186f
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58406:539cc471186f 58407:111d801b5d5d
   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