equal
deleted
inserted
replaced
6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** General *** |
10 *** General *** |
|
11 |
|
12 * Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to |
|
13 marginal comments in outer syntax. |
11 |
14 |
12 * The old 'def' command has been discontinued (legacy since |
15 * The old 'def' command has been discontinued (legacy since |
13 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with |
16 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with |
14 object-logic equality or equivalence. |
17 object-logic equality or equivalence. |
15 |
18 |