changeset 59518 | 28cfc60dea7a |
parent 58889 | 5b7a9633cfa8 |
child 60057 | 86fa63ce8156 |
--- 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 *}