--- a/src/HOL/equalities.ML Mon Feb 23 11:15:40 1998 +0100
+++ b/src/HOL/equalities.ML Mon Feb 23 11:16:18 1998 +0100
@@ -413,6 +413,11 @@
qed "UN_empty2";
Addsimps[UN_empty2];
+goal thy "(UN x:A. {x}) = A";
+by (Blast_tac 1);
+qed "UN_singleton";
+Addsimps [UN_singleton];
+
goal thy "!!k. k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
by (Blast_tac 1);
qed "UN_absorb";
@@ -609,6 +614,16 @@
by (Blast_tac 1);
qed "double_diff";
+goal thy "A Un (B-A) = A Un B";
+by (Blast_tac 1);
+qed "Un_Diff_cancel";
+
+goal thy "(B-A) Un A = B Un A";
+by (Blast_tac 1);
+qed "Un_Diff_cancel2";
+
+Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
+
goal thy "A - (B Un C) = (A-B) Int (A-C)";
by (Blast_tac 1);
qed "Diff_Un";
@@ -625,6 +640,10 @@
by (Blast_tac 1);
qed "Int_Diff";
+goal thy "(A-B) Int C = (A Int C) - (B Int C)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib";
+
section "Miscellany";