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