equal
deleted
inserted
replaced
760 lemmas [symmetric, rulify] = atomize_all atomize_imp |
760 lemmas [symmetric, rulify] = atomize_all atomize_imp |
761 and [symmetric, defn] = atomize_all atomize_imp atomize_eq |
761 and [symmetric, defn] = atomize_all atomize_imp atomize_eq |
762 |
762 |
763 |
763 |
764 subsubsection {* Atomizing elimination rules *} |
764 subsubsection {* Atomizing elimination rules *} |
765 |
|
766 setup AtomizeElim.setup |
|
767 |
765 |
768 lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" |
766 lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" |
769 by rule iprover+ |
767 by rule iprover+ |
770 |
768 |
771 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" |
769 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" |