src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Wed Feb 11 14:03:05 2015 +0100
+++ b/src/HOL/Relation.thy	Wed Feb 11 14:07:28 2015 +0100
@@ -426,6 +426,8 @@
   "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   by (simp add: trans_def transp_def)
 
+lemma transp_equality [simp]: "transp op ="
+by(auto intro: transpI)
 
 subsubsection {* Totality *}