# HG changeset patch
# User desharna
# Date 1742045359 -3600
# Node ID 7587b93032badc9d67dba9a86e60bbbeac96c3a3
# Parent  d260714c4f8ecdebba58018ed42bede8f287889f
proper theory name in NEWS

diff -r d260714c4f8e -r 7587b93032ba NEWS
--- a/NEWS	Sat Mar 15 14:10:23 2025 +0100
+++ b/NEWS	Sat Mar 15 14:29:19 2025 +0100
@@ -16,7 +16,7 @@
       monotone_on_inf_fun
       monotone_on_sup_fun
 
-* Theory "HOL.Relations":
+* Theory "HOL.Relation":
   - Changed definition of predicate refl_on to not constrain the domain
     and range of the relation. To get the old semantics, explicitely use
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
@@ -55,7 +55,7 @@
       quotient_disj_strong
 
 * Theory "HOL.Transfer":
-  - Moved right_unique from HOL.Transfer to HOL.Relations.
+  - Moved right_unique from HOL.Transfer to HOL.Relation.
     Minor INCOMPATIBILITY.
   - Added lemmas.
       single_valuedp_eq_right_unique