# HG changeset patch
# User desharna
# Date 1671434083 -3600
# Node ID a84716ca8b978c3e222d49d630b9d39c07a1e720
# Parent  10c4aa9eecf88db834d38139ec60f534edce8737
tuned naming

diff -r 10c4aa9eecf8 -r a84716ca8b97 src/HOL/Relation.thy
--- 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"