# HG changeset patch
# User wenzelm
# Date 963839168 -7200
# Node ID 12f251a5a3b5d88f9588fe55fd0351d9140ff5a3
# Parent  59dc5c4d1a57c457599a823a45edd292a6e4c6cb
AddXIs [UnI1, UnI2];

diff -r 59dc5c4d1a57 -r 12f251a5a3b5 src/HOL/Set.ML
--- 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";