src/HOL/equalities.ML
changeset 1618 372880456b5b
parent 1564 822575c737bd
child 1660 8cb42cd97579
     1.1 --- a/src/HOL/equalities.ML	Tue Mar 26 17:15:54 1996 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Mar 27 18:45:17 1996 +0100
     1.3 @@ -120,6 +120,10 @@
     1.4  by (fast_tac eq_cs 1);
     1.5  qed "Int_Un_distrib";
     1.6  
     1.7 +goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
     1.8 +by (fast_tac eq_cs 1);
     1.9 +qed "Int_Un_distrib2";
    1.10 +
    1.11  goal Set.thy "(A<=B) = (A Int B = A)";
    1.12  by (fast_tac (eq_cs addSEs [equalityE]) 1);
    1.13  qed "subset_Int_eq";