Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
strengthened and renamed lemma reflp_on_equality
authordesharna
Mon, 21 Nov 2022 13:53:04 +0100
changeset 76522 3fc92362fbb5
parent 76521 15f868460de9
child 76523 41c92fcb8805
strengthened and renamed lemma reflp_on_equality
NEWS file | annotate | diff | comparison | revisions
src/HOL/Relation.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Mon Nov 21 13:48:58 2022 +0100
+++ b/NEWS	Mon Nov 21 13:53:04 2022 +0100
@@ -26,8 +26,9 @@
     Minor INCOMPATIBILITY.
 
 * Theory "HOL.Relation":
-  - Strengthened lemmas. Minor INCOMPATIBILITY.
+  - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       total_on_singleton
+      reflp_equality[simp] ~> reflp_on_equality[simp]
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
--- a/src/HOL/Relation.thy	Mon Nov 21 13:48:58 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Nov 21 13:53:04 2022 +0100
@@ -246,8 +246,8 @@
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
-lemma reflp_equality [simp]: "reflp (=)"
-  by (simp add: reflp_def)
+lemma reflp_on_equality [simp]: "reflp_on A (=)"
+  by (simp add: reflp_on_def)
 
 lemma reflp_on_mono:
   "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
isabelle