# HG changeset patch
# User Andreas Lochbihler
# Date 1423660048 -3600
# Node ID 28cfc60dea7acc06e58d8899bdb457c53b0edf4a
# Parent  22c9e6cf5572c087b69da197cb7d6af102aac4f4
add lemma

diff -r 22c9e6cf5572 -r 28cfc60dea7a 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 *}