--- a/NEWS Tue Jan 03 11:30:37 2023 +0000
+++ b/NEWS Tue Jan 03 18:23:52 2023 +0100
@@ -74,11 +74,11 @@
antisymp_on_conversep[simp]
antisymp_on_if_asymp_on
antisymp_on_subset
- asym_on_iff_irrefl_on_if_trans
+ asym_on_iff_irrefl_on_if_trans_on
asym_onD
asym_onI
asym_on_converse[simp]
- asymp_on_iff_irreflp_on_if_transp
+ asymp_on_iff_irreflp_on_if_transp_on
asymp_onD
asymp_onI
asymp_on_asym_on_eq[pred_set_conv]
--- a/src/HOL/Relation.thy Tue Jan 03 11:30:37 2023 +0000
+++ b/src/HOL/Relation.thy Tue Jan 03 18:23:52 2023 +0100
@@ -718,11 +718,11 @@
lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
by (simp add: transp_def)
-lemma asym_on_iff_irrefl_on_if_trans: "trans r \<Longrightarrow> asym_on A r \<longleftrightarrow> irrefl_on A r"
- by (auto intro: irrefl_onI dest: transD asym_onD irrefl_onD)
+lemma asym_on_iff_irrefl_on_if_trans_on: "trans_on A r \<Longrightarrow> asym_on A r \<longleftrightarrow> irrefl_on A r"
+ by (auto intro: irrefl_on_if_asym_on dest: trans_onD irrefl_onD)
-lemma asymp_on_iff_irreflp_on_if_transp: "transp R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
- by (rule asym_on_iff_irrefl_on_if_trans[to_pred])
+lemma asymp_on_iff_irreflp_on_if_transp_on: "transp_on A R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
+ by (rule asym_on_iff_irrefl_on_if_trans_on[to_pred])
lemma (in preorder) transp_on_le[simp]: "transp_on A (\<le>)"
by (auto intro: transp_onI order_trans)