--- a/NEWS Wed Oct 11 14:03:16 2023 +0200
+++ b/NEWS Thu Oct 12 10:56:45 2023 +0200
@@ -33,6 +33,12 @@
INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.
+* Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML
+runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error.
+Exn.is_interrupt covers all kinds of interrupts as before, but
+Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more
+specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
+
*** HOL ***