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