equal
deleted
inserted
replaced
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** General *** |
10 *** General *** |
11 |
11 |
12 * Mixfix annotation syntax: "(\<open>unbreakable\<close>" supersedes "(00"; the old |
12 * Mixfix annotations support general block properties, with syntax |
13 form has been discontinued. INCOMPATIBILITY. |
13 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", |
|
14 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent |
|
15 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks |
|
16 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY. |
14 |
17 |
15 * New symbol \<circle>, e.g. for temporal operator. |
18 * New symbol \<circle>, e.g. for temporal operator. |
16 |
19 |
17 * Old 'header' command is no longer supported (legacy since |
20 * Old 'header' command is no longer supported (legacy since |
18 Isabelle2015). |
21 Isabelle2015). |