add lemma
authorAndreas Lochbihler
Wed Feb 11 14:07:28 2015 +0100 (2015-02-11)
changeset 5951828cfc60dea7a
parent 59517 22c9e6cf5572
child 59519 2fb0c0fc62a3
add lemma
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Wed Feb 11 14:03:05 2015 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Feb 11 14:07:28 2015 +0100
     1.3 @@ -426,6 +426,8 @@
     1.4    "transp r \<longleftrightarrow> trans {(x, y). r x y}"
     1.5    by (simp add: trans_def transp_def)
     1.6  
     1.7 +lemma transp_equality [simp]: "transp op ="
     1.8 +by(auto intro: transpI)
     1.9  
    1.10  subsubsection {* Totality *}
    1.11