# HG changeset patch
# User paulson
# Date 912505175 -3600
# Node ID 84fe61a08c1754f82796bae31d1a3fe29fe72640
# Parent  b2ecd577b8a35de69555ba968106ce12056dff13
new theorem INT_Un

diff -r b2ecd577b8a3 -r 84fe61a08c17 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Dec 01 10:39:02 1998 +0100
+++ b/src/HOL/equalities.ML	Tue Dec 01 10:39:35 1998 +0100
@@ -477,7 +477,7 @@
 qed "UN_insert";
 Addsimps[UN_insert];
 
-Goal "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
+Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
 by (Blast_tac 1);
 qed "UN_Un";
 
@@ -490,6 +490,10 @@
 qed "INT_insert";
 Addsimps[INT_insert];
 
+Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
+by (Blast_tac 1);
+qed "INT_Un";
+
 Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
 by (Blast_tac 1);
 qed "INT_insert_distrib";