src/ZF/equalities.ML

--- a/src/ZF/equalities.ML	Thu Apr 13 11:35:24 1995 +0200
+++ b/src/ZF/equalities.ML	Thu Apr 13 11:37:39 1995 +0200
@@ -67,6 +67,10 @@
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "subset_Int_iff2";
 
+goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
+by (fast_tac eq_cs 1);
+qed "Int_Diff_eq";
+
 (** Binary Union **)
 
 goal ZF.thy "0 Un A = A";