# HG changeset patch
# User wenzelm
# Date 1001599451 -7200
# Node ID d792570a04b181b783cf32f6ee05700647ed5c27
# Parent  cf448586f26abed08ff169cda4f982eef1290a59
AddXEs [disjI1, disjI2];

diff -r cf448586f26a -r d792570a04b1 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Thu Sep 27 15:42:30 2001 +0200
+++ b/src/FOL/FOL.ML	Thu Sep 27 16:04:11 2001 +0200
@@ -5,6 +5,7 @@
   val classical = classical;
 end;
 
-AddXIs [equal_intr_rule, disjI1, disjI2];
+AddXIs [equal_intr_rule];
+AddXEs [disjI1, disjI2];
 
 open FOL;
diff -r cf448586f26a -r d792570a04b1 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Thu Sep 27 15:42:30 2001 +0200
+++ b/src/HOL/HOL.ML	Thu Sep 27 16:04:11 2001 +0200
@@ -29,7 +29,7 @@
   val arbitrary_def = arbitrary_def;
 end;
 
-AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex, sym];
+AddXIs [equal_intr_rule, ext];
+AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
 
 open HOL;