# HG changeset patch
# User wenzelm
# Date 969636276 -7200
# Node ID 3b819da9c71a71f0a7f87506b396c4dba55b38c2
# Parent  fe82134773dc86f967ad88c83a99792a2318a0d0
AddXIs [equal_intr_rule];

diff -r fe82134773dc -r 3b819da9c71a src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Fri Sep 22 16:28:53 2000 +0200
+++ b/src/FOL/FOL.ML	Fri Sep 22 17:24:36 2000 +0200
@@ -5,6 +5,6 @@
   val classical = classical;
 end;
 
-AddXIs [disjI1, disjI2];
+AddXIs [equal_intr_rule, disjI1, disjI2];
 
 open FOL;
diff -r fe82134773dc -r 3b819da9c71a src/HOL/HOL.ML
--- 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;