# HG changeset patch
# User wenzelm
# Date 1004561884 -3600
# Node ID c09427e5f55497d3df5d8051f2283254a4b37ba7
# Parent  bc9b5bad0e7bc451c0666764249c1be23f4ccba4
removed obsolete (rule equal_intr_rule);

diff -r bc9b5bad0e7b -r c09427e5f554 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 31 20:00:35 2001 +0100
+++ b/src/HOL/HOL.thy	Wed Oct 31 21:58:04 2001 +0100
@@ -206,7 +206,7 @@
 subsubsection {* Atomizing meta-level connectives *}
 
 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
@@ -215,7 +215,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
@@ -224,7 +224,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
@@ -233,7 +233,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