equal_intr_rule already declared in Pure;
authorwenzelm
Sun Oct 28 21:10:47 2001 +0100 (2001-10-28)
changeset 11976075df6e46cef
parent 11975 129c6679e8c4
child 11977 2e7c54b86763
equal_intr_rule already declared in Pure;
src/FOL/FOL.ML
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/FOL.ML	Sun Oct 28 19:44:58 2001 +0100
     1.2 +++ b/src/FOL/FOL.ML	Sun Oct 28 21:10:47 2001 +0100
     1.3 @@ -5,7 +5,6 @@
     1.4    val classical = classical;
     1.5  end;
     1.6  
     1.7 -AddXIs [equal_intr_rule];
     1.8  AddXEs [disjI1, disjI2];
     1.9  
    1.10  open FOL;
     2.1 --- a/src/FOL/IFOL.thy	Sun Oct 28 19:44:58 2001 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Sun Oct 28 21:10:47 2001 +0100
     2.3 @@ -132,7 +132,7 @@
     2.4  subsection {* Atomizing meta-level rules *}
     2.5  
     2.6  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
     2.7 -proof (rule equal_intr_rule)
     2.8 +proof
     2.9    assume "!!x. P(x)"
    2.10    show "ALL x. P(x)" by (rule allI)
    2.11  next
    2.12 @@ -141,7 +141,7 @@
    2.13  qed
    2.14  
    2.15  lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
    2.16 -proof (rule equal_intr_rule)
    2.17 +proof
    2.18    assume r: "A ==> B"
    2.19    show "A --> B" by (rule impI) (rule r)
    2.20  next
    2.21 @@ -150,7 +150,7 @@
    2.22  qed
    2.23  
    2.24  lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
    2.25 -proof (rule equal_intr_rule)
    2.26 +proof
    2.27    assume "x == y"
    2.28    show "x = y" by (unfold prems) (rule refl)
    2.29  next
    2.30 @@ -159,7 +159,7 @@
    2.31  qed
    2.32  
    2.33  lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    2.34 -proof (rule equal_intr_rule)
    2.35 +proof
    2.36    assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
    2.37    show "A & B" by (rule conjI)
    2.38  next