# HG changeset patch
# User wenzelm
# Date 1711484735 -3600
# Node ID 339325fdb128104e3935e67085362bd733a0bc36
# Parent  6d01661a055bd30f6601efcacf46d06a9f04c89c
misc tuning for release;

diff -r 6d01661a055b -r 339325fdb128 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Mar 26 21:16:47 2024 +0100
+++ b/CONTRIBUTORS	Tue Mar 26 21:25:35 2024 +0100
@@ -3,24 +3,24 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2024
+-----------------------------
 
 * March 2024: Manuel Eberl
-  Weierstraß Factorization Theorem in HOL-Complex_Analysis
+  Weierstraß Factorization Theorem in HOL-Complex_Analysis.
 
 * March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson
-  New and more general definition of meromorphicity in HOL-Complex_Analysis
+  New and more general definition of meromorphicity in HOL-Complex_Analysis.
 
 * Feb/March 2024: Jonas Stahl
-  Automatic translation of HOL functions into corresponding
-  step-counting running-time functions
+  Automatic translation of HOL functions into corresponding step-counting
+  running-time functions.
 
 * 2023/2024: Makarius Wenzel and Fabian Huch
   More robust and scalable support for distributed build clusters.
 
 * October 2023: Fabian Huch
-  Support for SMTP mailing.
+  Support for SMTP mailing in Isabelle/Scala.
 
 
 Contributions to Isabelle2023
diff -r 6d01661a055b -r 339325fdb128 NEWS
--- a/NEWS	Tue Mar 26 21:16:47 2024 +0100
+++ b/NEWS	Tue Mar 26 21:25:35 2024 +0100
@@ -4,8 +4,8 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2024 (May 2024)
+------------------------------
 
 *** General ***
 
@@ -31,6 +31,14 @@
 (02-Nov-2023). See also src/Doc/Demo_LLNCS/.
 
 
+*** Pure ***
+
+* Added configuration option "unify_trace" (default: false) to guard
+tracing of higher-order unification, which is ubiquitous in assumption
+steps and rule applications via resolution. This is disabled by default
+to avoid breakdown due to massive amounts of spurious messages.
+
+
 *** HOL ***
 
 * Commands 'inductive_cases', 'inductive_simps', 'case_of_simps',
@@ -46,16 +54,13 @@
   - Added support for "order" proof method to proof reconstruction.
 
 * Mirabelle:
-  - Removed proof reconstruction from "sledgehammer" action;
-    the related option "proof_method" was removed. Proof reconstruction is
-    supported directly by Sledgehammer and should be used instead. For
-    more information, see Sledgehammer's documentation relating to
+  - Removed proof reconstruction from "sledgehammer" action; the related
+    option "proof_method" was removed. Proof reconstruction is supported
+    directly by Sledgehammer and should be used instead. For more
+    information, see Sledgehammer's documentation relating to
     "preplay_timeout". INCOMPATIBILITY.
   - Added the action "order" testing the proof method of the same name.
 
-* Session Data_Structures provides automatic translation from
-HOL functions into corresponding step-counting running-time functions.See theory Define_Time_Function.
-
 * Explicit type class for discrete_linear_ordered_semidom for integral
 semidomains with a discrete linear order.
 
@@ -107,11 +112,12 @@
       tranclp_less_eq[simp]
 
 * Theory "HOL.Wellfounded":
-  - Added predicates wf_on and wfp_on and redefined wfP to be abbreviations.
-    Lemmas wf_def and wfP_def are explicitly provided for backward
-    compatibility but their usage is discouraged. Minor INCOMPATIBILITY.
-  - Added wfp as alias for wfP for greater consistency with other predicates
-    such as asymp, transp, or totalp.
+  - Added predicates wf_on and wfp_on and redefined wfP to be
+    abbreviations. Lemmas wf_def and wfP_def are explicitly provided for
+    backward compatibility but their usage is discouraged. Minor
+    INCOMPATIBILITY.
+  - Added wfp as alias for wfP for greater consistency with other
+    predicates such as asymp, transp, or totalp.
   - Added lemmas.
       wellorder.wfp_on_less[simp]
       wfP_iff_ex_minimal
@@ -148,12 +154,9 @@
 * HOL-Complex_Analysis: new, more general definition of meromorphicity.
 INCOMPATIBILITY.
 
-*** Pure ***
-
-* Added configuration option "unify_trace" (default: false) to guard
-tracing of higher-order unification, which is ubiquitous in assumption
-steps and rule applications via resolution. This is disabled by default
-to avoid breakdown due to massive amounts of spurious messages.
+* HOL-Data_Structures: automatic translation from HOL functions into
+corresponding step-counting running-time functions. See theory
+"HOL-Data_Structures.Define_Time_Function".
 
 
 *** ML ***