diff -r ab78019b8ec8 -r 1a038ec6f923 src/ZF/equalities.ML
--- 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);