src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Tue Aug 26 16:36:30 2008 +0200
+++ b/src/HOL/Relation.thy	Tue Aug 26 18:59:52 2008 +0200
@@ -166,6 +166,12 @@
     "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
 by blast
 
+lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
+by auto
+
+lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
+by auto
+
 
 subsection {* Reflexivity *}