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