# HG changeset patch
# User paulson
# Date 903428713 -7200
# Node ID 3d27b96a08b02ad0c7d5a97cb09769f7e6b3019d
# Parent  8c9fadda81f4d59b18709bce58587450f6452576
new theorem Un_Diff_Int

diff -r 8c9fadda81f4 -r 3d27b96a08b0 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Aug 18 10:24:54 1998 +0200
+++ b/src/HOL/equalities.ML	Tue Aug 18 10:25:13 1998 +0200
@@ -331,6 +331,10 @@
 by (Blast_tac 1);
 qed "Un_subset_iff";
 
+Goal "(A - B) Un (A Int B) = A";
+by (Blast_tac 1);
+qed "Un_Diff_Int";
+
 
 section "Compl";