--- 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";