removed obsolete (rule equal_intr_rule);
authorwenzelm
Wed Oct 31 21:58:04 2001 +0100 (2001-10-31)
changeset 12003c09427e5f554
parent 12002 bc9b5bad0e7b
child 12004 1703de633aaf
removed obsolete (rule equal_intr_rule);
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 31 20:00:35 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 31 21:58:04 2001 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4  subsubsection {* Atomizing meta-level connectives *}
     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 @@ -215,7 +215,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 @@ -224,7 +224,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 @@ -233,7 +233,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