equal
deleted
inserted
replaced
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 |
33 |
34 * Mixfix annotations may use cartouches instead of old-style double |
34 * Mixfix annotations may use cartouches instead of old-style double |
35 quotes, e.g. (infixl \<open>+\<close> 60). |
35 quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u |
|
36 mixfix_cartouches" allows to update existing theory sources |
|
37 automatically. |
36 |
38 |
37 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
39 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
38 need to provide a closed expression -- without trailing semicolon. Minor |
40 need to provide a closed expression -- without trailing semicolon. Minor |
39 INCOMPATIBILITY. |
41 INCOMPATIBILITY. |
40 |
42 |