src/FOL/IFOL.thy
changeset 11953 f98623fdf6ef
parent 11848 6e3017adb8c0
child 11976 075df6e46cef
     1.1 --- a/src/FOL/IFOL.thy	Fri Oct 26 23:58:21 2001 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Fri Oct 26 23:59:13 2001 +0200
     1.3 @@ -158,6 +158,21 @@
     1.4    thus "x == y" by (rule eq_reflection)
     1.5  qed
     1.6  
     1.7 +lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
     1.8 +proof (rule equal_intr_rule)
     1.9 +  assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    1.10 +  show "A & B" by (rule conjI)
    1.11 +next
    1.12 +  fix C
    1.13 +  assume "A & B"
    1.14 +  assume "A ==> B ==> PROP C"
    1.15 +  thus "PROP C"
    1.16 +  proof this
    1.17 +    show A by (rule conjunct1)
    1.18 +    show B by (rule conjunct2)
    1.19 +  qed
    1.20 +qed
    1.21 +
    1.22  declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
    1.23  
    1.24