# HG changeset patch
# User wenzelm
# Date 1004299847 -3600
# Node ID 075df6e46cef745f60f3da6512018ad6727a57ee
# Parent  129c6679e8c40cb1793f0e9a12950dd50f7e9673
equal_intr_rule already declared in Pure;

diff -r 129c6679e8c4 -r 075df6e46cef src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Sun Oct 28 19:44:58 2001 +0100
+++ b/src/FOL/FOL.ML	Sun Oct 28 21:10:47 2001 +0100
@@ -5,7 +5,6 @@
   val classical = classical;
 end;
 
-AddXIs [equal_intr_rule];
 AddXEs [disjI1, disjI2];
 
 open FOL;
diff -r 129c6679e8c4 -r 075df6e46cef src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Oct 28 19:44:58 2001 +0100
+++ b/src/FOL/IFOL.thy	Sun Oct 28 21:10:47 2001 +0100
@@ -132,7 +132,7 @@
 subsection {* Atomizing meta-level rules *}
 
 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
-proof (rule equal_intr_rule)
+proof
   assume "!!x. P(x)"
   show "ALL x. P(x)" by (rule allI)
 next
@@ -141,7 +141,7 @@
 qed
 
 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
-proof (rule equal_intr_rule)
+proof
   assume r: "A ==> B"
   show "A --> B" by (rule impI) (rule r)
 next
@@ -150,7 +150,7 @@
 qed
 
 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
-proof (rule equal_intr_rule)
+proof
   assume "x == y"
   show "x = y" by (unfold prems) (rule refl)
 next
@@ -159,7 +159,7 @@
 qed
 
 lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
-proof (rule equal_intr_rule)
+proof
   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   show "A & B" by (rule conjI)
 next