--- a/NEWS Tue Dec 20 08:41:01 2022 +0100
+++ b/NEWS Mon Dec 19 15:36:45 2022 +0100
@@ -110,6 +110,7 @@
totalI
totalp_on_converse[simp]
totalp_on_singleton[simp]
+ transp_on_trans_on_eq[pred_set_conv]
* Theory "HOL.Transitive_Closure":
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
--- a/src/HOL/Relation.thy Tue Dec 20 08:41:01 2022 +0100
+++ b/src/HOL/Relation.thy Mon Dec 19 15:36:45 2022 +0100
@@ -623,8 +623,10 @@
text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close>
-lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
- by (simp add: trans_def transp_def)
+lemma transp_on_trans_on_eq[pred_set_conv]: "transp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans_on A r"
+ by (simp add: trans_on_def transp_on_def)
+
+lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
by (unfold trans_def) iprover