# HG changeset patch
# User wenzelm
# Date 1001599465 -7200
# Node ID 9a6d4511bb3c969575af706b84defe842ee9c642
# Parent  d792570a04b181b783cf32f6ee05700647ed5c27
AddXEs [UnI1, UnI2];

diff -r d792570a04b1 -r 9a6d4511bb3c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Sep 27 16:04:11 2001 +0200
+++ b/src/HOL/Set.ML	Thu Sep 27 16:04:25 2001 +0200
@@ -422,7 +422,7 @@
 by (Asm_simp_tac 1);
 qed "UnI2";
 
-AddXIs [UnI1, UnI2];
+AddXEs [UnI1, UnI2];
 
 
 (*Classical introduction rule: no commitment to A vs B*)
diff -r d792570a04b1 -r 9a6d4511bb3c src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Sep 27 16:04:11 2001 +0200
+++ b/src/ZF/upair.ML	Thu Sep 27 16:04:25 2001 +0200
@@ -84,6 +84,7 @@
 
 AddSIs [UnCI];
 AddSEs [UnE];
+AddXEs [UnI1, UnI2];
 
 
 (*** Rules for small intersection -- Int -- defined via Upair ***)