AddXIs [UnI1, UnI2];

--- a/src/HOL/Set.ML	Mon Jul 17 14:02:09 2000 +0200
+++ b/src/HOL/Set.ML	Mon Jul 17 15:06:08 2000 +0200
@@ -369,6 +369,9 @@
 by (Asm_simp_tac 1);
 qed "UnI2";
 
+AddXIs [UnI1, UnI2];
+
+
 (*Classical introduction rule: no commitment to A vs B*)
 
 val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";