# HG changeset patch
# User paulson
# Date 880020206 -3600
# Node ID 97601cf262621c22971e2f02a5b10cd258ba685f
# Parent  3f3f87c6fe3b6053f22746fd432e5c78ff1d412e
Two new rewrites

diff -r 3f3f87c6fe3b -r 97601cf26262 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Nov 20 10:55:27 1997 +0100
+++ b/src/ZF/equalities.ML	Thu Nov 20 11:03:26 1997 +0100
@@ -245,6 +245,17 @@
 by (Blast_tac 1);
 qed "INT_constant";
 
+goal ZF.thy "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
+by (Blast_tac 1);
+qed "UN_RepFun";
+
+goal ZF.thy "!!x. x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
+by (Blast_tac 1);
+qed "INT_RepFun";
+
+Addsimps [UN_RepFun, INT_RepFun];
+
+
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     Union of a family of unions **)