# HG changeset patch
# User wenzelm
# Date 1752576352 -7200
# Node ID bc969aed0c7f06bfffdcd30c4587cf612a5ce71f
# Parent  9a19d83dfd5c0fcb1d7f62cd70e6326afd39993d
NEWS;

diff -r 9a19d83dfd5c -r bc969aed0c7f NEWS
--- a/NEWS	Tue Jul 15 12:40:08 2025 +0200
+++ b/NEWS	Tue Jul 15 12:45:52 2025 +0200
@@ -16,6 +16,16 @@
 state output (if enabled). This affects Isabelle/jEdit panels for Output
 vs. State in particular.
 
+* Declarations of intro/elim/dest rules for Pure and the Classical
+Reasoner (e.g. HOL) are handled more uniformly and efficiently: the
+order of rule declarations is maintained accurately, regardless of
+intermediate [rule del] declarations. Furthermore, [dest] is now a
+proper declaration on its own account, instead of the former expansion
+[elim_format, elim]. Consequently, [rule del] no longer deletes the
+[elim_format] of the given rule, only the original rule. Rare
+INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual
+situations.
+
 * A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
 now able to load markup and messages from the underlying session
 database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory