--- a/src/HOL/HOL.ML Fri Sep 22 16:28:53 2000 +0200
+++ b/src/HOL/HOL.ML Fri Sep 22 17:24:36 2000 +0200
@@ -31,6 +31,7 @@
val arbitrary_def = arbitrary_def;
end;
-AddXIs [disjI1, disjI2, ext];
+AddXIs [equal_intr_rule, disjI1, disjI2, ext];
+AddXEs [ex1_implies_ex];
open HOL;