# HG changeset patch
# User paulson
# Date 888934377 -3600
# Node ID 248b876c2fa8d3b536b0ea56710694f5c4695e32
# Parent  59d80bacee6281fc864cc7d0ee3e64eeea96ae6a
New theorems

diff -r 59d80bacee62 -r 248b876c2fa8 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Tue Mar 03 15:12:25 1998 +0100
+++ b/src/HOL/Vimage.ML	Tue Mar 03 15:12:57 1998 +0100
@@ -46,7 +46,11 @@
 by (Blast_tac 1);
 qed "vimage_Un";
 
-Addsimps [vimage_empty, vimage_Compl, vimage_Un];
+goal thy "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_UN";
+
+Addsimps [vimage_empty, vimage_Un];
 
 (*NOT suitable for rewriting because of the recurrence of {a}*)
 goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
diff -r 59d80bacee62 -r 248b876c2fa8 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Mar 03 15:12:25 1998 +0100
+++ b/src/HOL/equalities.ML	Tue Mar 03 15:12:57 1998 +0100
@@ -504,6 +504,10 @@
 by (Blast_tac 1);
 qed "Int_Union";
 
+goal thy "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
    Union of a family of unions **)
 goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
@@ -573,6 +577,10 @@
 qed "Diff_cancel";
 Addsimps[Diff_cancel];
 
+goal thy "!!A B. A Int B = {} ==> A-B = A";
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "Diff_triv";
+
 goal thy "{}-A = {}";
 by (Blast_tac 1);
 qed "empty_Diff";