| changeset 67352 | 5f7f339f3d7e |
| parent 67341 | df79ef3b3a41 |
| child 67356 | ba226b87c69e |
--- a/NEWS Sat Jan 06 15:08:42 2018 +0100 +++ b/NEWS Sat Jan 06 16:56:07 2018 +0100 @@ -9,6 +9,9 @@ *** General *** +* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to +marginal comments in outer syntax. + * The old 'def' command has been discontinued (legacy since Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with object-logic equality or equivalence.