--- a/NEWS Sat Oct 08 18:35:53 2022 +0200
+++ b/NEWS Sun Oct 09 16:10:52 2022 +0200
@@ -7,6 +7,12 @@
New in this Isabelle version
----------------------------
+*** HOL ***
+
+* Theory "HOL.Relation":
+ - Strengthened total_on_singleton. Minor INCOMPATIBILITY.
+ - Added lemma.
+ totalp_on_singleton[simp]
New in Isabelle2022 (October 2022)
--- a/src/HOL/Relation.thy Sat Oct 08 18:35:53 2022 +0200
+++ b/src/HOL/Relation.thy Sun Oct 09 16:10:52 2022 +0200
@@ -555,10 +555,13 @@
by (simp add: total_on_def)
lemma totalp_on_empty [simp]: "totalp_on {} R"
- by (auto intro: totalp_onI)
+ by (simp add: totalp_on_def)
-lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
- unfolding total_on_def by blast
+lemma total_on_singleton [simp]: "total_on {x} r"
+ by (simp add: total_on_def)
+
+lemma totalp_on_singleton [simp]: "totalp_on {x} R"
+ by (simp add: totalp_on_def)
subsubsection \<open>Single valued relations\<close>