AddXIs [UnI1, UnI2];
authorwenzelm
Mon Jul 17 15:06:08 2000 +0200 (2000-07-17)
changeset 937812f251a5a3b5
parent 9377 59dc5c4d1a57
child 9379 21cfeae6659d
AddXIs [UnI1, UnI2];
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Mon Jul 17 14:02:09 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Jul 17 15:06:08 2000 +0200
     1.3 @@ -369,6 +369,9 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "UnI2";
     1.6  
     1.7 +AddXIs [UnI1, UnI2];
     1.8 +
     1.9 +
    1.10  (*Classical introduction rule: no commitment to A vs B*)
    1.11  
    1.12  val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";