# HG changeset patch
# User wenzelm
# Date 971214203 -7200
# Node ID 5413bcce14821d3dc55537d0795085a4b3454fb5
# Parent  c07860c826c524ba798e38b164b89802aec8b808
AddXEs [someI_ex];

diff -r c07860c826c5 -r 5413bcce1482 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Tue Oct 10 12:31:00 2000 +0200
+++ b/src/HOL/HOL.ML	Tue Oct 10 23:43:23 2000 +0200
@@ -32,6 +32,6 @@
 end;
 
 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex];
+AddXEs [ex1_implies_ex, someI_ex];
 
 open HOL;