--- 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