# HG changeset patch
# User wenzelm
# Date 1004300096 -3600
# Node ID 2e7c54b867638ebc7805c3f1cea87ed5c59c336f
# Parent  075df6e46cef745f60f3da6512018ad6727a57ee
tuned declaration of rules;

diff -r 075df6e46cef -r 2e7c54b86763 src/HOL/HOL.ML
--- 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";
diff -r 075df6e46cef -r 2e7c54b86763 src/HOL/HOL.thy
--- 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