# HG changeset patch
# User paulson
# Date 890657813 -3600
# Node ID 2b8ead8e9393bcbd50604d0f678ebdbe27bb8d7f
# Parent  bbe14a54deb3107a4c53d50a148e147069e2ebca
more thms

diff -r bbe14a54deb3 -r 2b8ead8e9393 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Mar 16 16:54:07 1998 +0100
+++ b/src/HOL/equalities.ML	Mon Mar 23 13:56:53 1998 +0100
@@ -27,6 +27,15 @@
 qed "not_psubset_empty";
 AddIffs [not_psubset_empty];
 
+goal thy "{x. P x | Q x} = {x. P x} Un {x. Q x}";
+by (Blast_tac 1);
+qed "Collect_disj_eq";
+
+goal thy "{x. P x & Q x} = {x. P x} Int {x. Q x}";
+by (Blast_tac 1);
+qed "Collect_conj_eq";
+
+
 section "insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
@@ -664,9 +673,13 @@
 by (Blast_tac 1);
 qed "Int_Diff";
 
+goal thy "C Int (A-B) = (C Int A) - (C Int B)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib";
+
 goal thy "(A-B) Int C = (A Int C) - (B Int C)";
 by (Blast_tac 1);
-qed "Diff_Int_distrib";
+qed "Diff_Int_distrib2";
 
 
 section "Miscellany";