# HG changeset patch
# User krauss
# Date 1273399243 -7200
# Node ID ef97c50068402553a9bc714fab6987826cf45699
# Parent  3e08b6789e66b3bcf85ba424079271778c2e708e
added lemmas rel_comp_UNION_distrib(2)

diff -r 3e08b6789e66 -r ef97c5006840 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat May 08 22:29:44 2010 +0200
+++ b/src/HOL/Relation.thy	Sun May 09 12:00:43 2010 +0200
@@ -181,6 +181,12 @@
 lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
 by auto
 
+lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
+by auto
+
+lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
+by auto
+
 
 subsection {* Reflexivity *}