# HG changeset patch
# User lcp
# Date 797765859 -7200
# Node ID 279a4fd3c5ce477fc90513b9754aec56452b1de3
# Parent  ccc9a3cbca05b70ee8cc13c9a742e91170f6bee6
Proved Int_Diff_eq.

diff -r ccc9a3cbca05 -r 279a4fd3c5ce 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";