--- a/src/HOL/HOL.ML Thu Oct 19 21:20:07 2000 +0200
+++ b/src/HOL/HOL.ML Thu Oct 19 21:20:53 2000 +0200
@@ -32,6 +32,6 @@
end;
AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex, someI_ex];
+AddXEs [ex1_implies_ex, someI_ex, sym];
open HOL;