summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOL/IFOL.thy

changeset 11953 | f98623fdf6ef |

parent 11848 | 6e3017adb8c0 |

child 11976 | 075df6e46cef |

--- a/src/FOL/IFOL.thy Fri Oct 26 23:58:21 2001 +0200 +++ b/src/FOL/IFOL.thy Fri Oct 26 23:59:13 2001 +0200 @@ -158,6 +158,21 @@ thus "x == y" by (rule eq_reflection) qed +lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" +proof (rule equal_intr_rule) + assume "!!C. (A ==> B ==> PROP C) ==> PROP C" + show "A & B" by (rule conjI) +next + fix C + assume "A & B" + assume "A ==> B ==> PROP C" + thus "PROP C" + proof this + show A by (rule conjunct1) + show B by (rule conjunct2) + qed +qed + declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]