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