--- a/src/ZF/equalities.ML Wed Feb 09 14:25:29 1994 +0100
+++ b/src/ZF/equalities.ML Mon Feb 14 17:59:25 1994 +0100
@@ -120,10 +120,14 @@
by (fast_tac eq_cs 1);
val Diff_partition = result();
-goal ZF.thy "!!A B. [| A<=B; B<= C |] ==> (B - (C-A)) = A";
+goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
by (fast_tac eq_cs 1);
val double_complement = result();
+goal ZF.thy "(A Un B) - (B-A) = A";
+by (fast_tac eq_cs 1);
+val double_complement_Un = result();
+
goal ZF.thy
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
by (fast_tac eq_cs 1);