NEWS
changeset 67356 ba226b87c69e
parent 67352 5f7f339f3d7e
child 67368 e9bee1ddfe19
     1.1 --- a/NEWS	Sun Jan 07 12:41:34 2018 +0100
     1.2 +++ b/NEWS	Sun Jan 07 13:45:21 2018 +0100
     1.3 @@ -10,7 +10,8 @@
     1.4  *** General ***
     1.5  
     1.6  * Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
     1.7 -marginal comments in outer syntax.
     1.8 +marginal comments in outer syntax: antiquotations are supported as usual
     1.9 +(wrt. the overall command context).
    1.10  
    1.11  * The old 'def' command has been discontinued (legacy since
    1.12  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with