equal
deleted
inserted
replaced
28 * Old-style inner comments (* ... *) within the term language are no |
28 * Old-style inner comments (* ... *) within the term language are no |
29 longer supported (legacy feature in Isabelle2018). |
29 longer supported (legacy feature in Isabelle2018). |
30 |
30 |
31 * Infix operators that begin or end with a "*" can now be paranthesized |
31 * Infix operators that begin or end with a "*" can now be paranthesized |
32 without additional spaces, eg "(*)" instead of "( * )". |
32 without additional spaces, eg "(*)" instead of "( * )". |
|
33 |
|
34 * Mixfix annotations may use cartouches instead of old-style double |
|
35 quotes, e.g. (infixl \<open>+\<close> 60). |
33 |
36 |
34 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
37 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
35 need to provide a closed expression -- without trailing semicolon. Minor |
38 need to provide a closed expression -- without trailing semicolon. Minor |
36 INCOMPATIBILITY. |
39 INCOMPATIBILITY. |
37 |
40 |