--- a/src/HOL/Relation.thy Mon Dec 19 08:14:23 2022 +0100
+++ b/src/HOL/Relation.thy Mon Dec 19 08:14:43 2022 +0100
@@ -378,7 +378,7 @@
lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
by (rule asymD[to_pred])
-lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
+lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
by (blast dest: asymD)
lemma asym_on_subset: "asym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asym_on B r"