NEWS
changeset 78728 72631efa3821
parent 78622 c42f316f0a01
child 78729 fc0814e9f7a8
--- a/NEWS	Thu Sep 28 19:40:20 2023 +0200
+++ b/NEWS	Thu Sep 28 20:07:30 2023 +0200
@@ -14,6 +14,13 @@
 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
 
 
+*** ML ***
+
+* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
+INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
+as last resort declare [[ML_catch_all]] within the theory context.
+
+
 
 New in Isabelle2023 (September 2023)
 ------------------------------------