tuned variable names
authordesharna
Mon, 24 Mar 2025 14:09:48 +0100 (2 weeks ago)
changeset 82334 fce6872bd4d2
parent 82333 06c1c163b66c
child 82335 3bdfdadf3a52
tuned variable names
src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 14:09:05 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 14:09:48 2025 +0100
@@ -216,7 +216,7 @@
 lemma reflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> reflp_on B R \<le> reflp_on A Q"
   by (simp add: reflp_on_mono_strong le_fun_def)
 
-lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
+lemma reflp_on_subset: "reflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> reflp_on A R"
   using reflp_on_mono_strong .
 
 lemma reflp_on_image: "reflp_on (f ` A) R \<longleftrightarrow> reflp_on A (\<lambda>a b. R (f a) (f b))"