equal
deleted
inserted
replaced
10 *** System *** |
10 *** System *** |
11 |
11 |
12 * Isabelle/Scala and derived Scala tools now use the syntax of Scala |
12 * Isabelle/Scala and derived Scala tools now use the syntax of Scala |
13 3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as |
13 3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as |
14 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY. |
14 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY. |
|
15 |
|
16 |
|
17 *** ML *** |
|
18 |
|
19 * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. |
|
20 INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or |
|
21 as last resort declare [[ML_catch_all]] within the theory context. |
15 |
22 |
16 |
23 |
17 |
24 |
18 New in Isabelle2023 (September 2023) |
25 New in Isabelle2023 (September 2023) |
19 ------------------------------------ |
26 ------------------------------------ |