equal
deleted
inserted
replaced
11 |
11 |
12 * Marginal comments need to be written exclusively in the new-style form |
12 * Marginal comments need to be written exclusively in the new-style form |
13 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
13 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
14 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
14 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
15 update_comments" to update existing theory files. |
15 update_comments" to update existing theory files. |
|
16 |
|
17 * Old-style inner comments (* ... *) within the term language are legacy |
|
18 and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>" |
|
19 instead. |
16 |
20 |
17 * The "op <infix-op>" syntax for infix operators has been replaced by |
21 * The "op <infix-op>" syntax for infix operators has been replaced by |
18 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to |
22 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to |
19 be a space between the "*" and the corresponding parenthesis. |
23 be a space between the "*" and the corresponding parenthesis. |
20 INCOMPATIBILITY. |
24 INCOMPATIBILITY. |