src/FOL/IFOL.thy
changeset 11976 075df6e46cef
parent 11953 f98623fdf6ef
child 12019 abe9b7c6016e
     1.1 --- a/src/FOL/IFOL.thy	Sun Oct 28 19:44:58 2001 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Sun Oct 28 21:10:47 2001 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4  subsection {* Atomizing meta-level rules *}
     1.5  
     1.6  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
     1.7 -proof (rule equal_intr_rule)
     1.8 +proof
     1.9    assume "!!x. P(x)"
    1.10    show "ALL x. P(x)" by (rule allI)
    1.11  next
    1.12 @@ -141,7 +141,7 @@
    1.13  qed
    1.14  
    1.15  lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
    1.16 -proof (rule equal_intr_rule)
    1.17 +proof
    1.18    assume r: "A ==> B"
    1.19    show "A --> B" by (rule impI) (rule r)
    1.20  next
    1.21 @@ -150,7 +150,7 @@
    1.22  qed
    1.23  
    1.24  lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
    1.25 -proof (rule equal_intr_rule)
    1.26 +proof
    1.27    assume "x == y"
    1.28    show "x = y" by (unfold prems) (rule refl)
    1.29  next
    1.30 @@ -159,7 +159,7 @@
    1.31  qed
    1.32  
    1.33  lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    1.34 -proof (rule equal_intr_rule)
    1.35 +proof
    1.36    assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    1.37    show "A & B" by (rule conjI)
    1.38  next