src/HOL/Relation.thy
changeset 55083 0a689157e3ce
parent 54611 31afce809794
child 55096 916b2ac758f4
     1.1 --- a/src/HOL/Relation.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -624,6 +624,9 @@
     1.4    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
     1.5    by (auto simp add: set_eq_iff)
     1.6  
     1.7 +lemma eq_OO: "op= OO R = R"
     1.8 +by blast
     1.9 +
    1.10  
    1.11  subsubsection {* Converse *}
    1.12