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