tuned declaration of rules;

--- a/src/HOL/HOL.ML	Sun Oct 28 21:10:47 2001 +0100
+++ b/src/HOL/HOL.ML	Sun Oct 28 21:14:56 2001 +0100
@@ -29,9 +29,6 @@
   val arbitrary_def = arbitrary_def;
 end;
 
-AddXIs [equal_intr_rule, ext];
-AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
-
 open HOL;
 
 val Least_def = thm "Least_def";

--- a/src/HOL/HOL.thy	Sun Oct 28 21:10:47 2001 +0100
+++ b/src/HOL/HOL.thy	Sun Oct 28 21:14:56 2001 +0100
@@ -252,10 +252,15 @@
 
 use "cladata.ML"
 setup hypsubst_setup
+
 declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
+
 setup Classical.setup
 setup clasetup
 
+declare ext [intro?]
+declare disjI1 [elim?]  disjI2 [elim?]  ex1_implies_ex [elim?]  sym [elim?]
+
 use "blastdata.ML"
 setup Blast.setup