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