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