# HG changeset patch
# User wenzelm
# Date 1741878048 -3600
# Node ID 72e641e3b7cd19acbd6eaebf315f2acea09cfcc5
# Parent  afc1d2b349d8afc97acbec9e81f7157f055260b0
proper document structure;
tuned whitespace;

diff -r afc1d2b349d8 -r 72e641e3b7cd NEWS
--- a/NEWS	Thu Mar 13 15:56:32 2025 +0100
+++ b/NEWS	Thu Mar 13 16:00:48 2025 +0100
@@ -7,6 +7,8 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun
@@ -15,9 +17,9 @@
       monotone_on_sup_fun
 
 * Theory "HOL.Relations":
-  - 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 ⊂ A × A ∧ refl_on A r". INCOMPATIBILITY.
+  - 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.
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
@@ -55,6 +57,7 @@
       size_mset_sum_mset_conv[simp]
 
 
+
 New in Isabelle2025 (March 2025)
 --------------------------------