NEWS
changeset 67507 5db077cfe1b2
parent 67448 dbb1f02e667d
child 67510 9624711ef2de
     1.1 --- a/NEWS	Thu Jan 25 15:21:05 2018 +0100
     1.2 +++ b/NEWS	Thu Jan 25 16:01:02 2018 +0100
     1.3 @@ -14,6 +14,10 @@
     1.4  supported. INCOMPATIBILITY, use the command-line tool "isabelle
     1.5  update_comments" to update existing theory files.
     1.6  
     1.7 +* Old-style inner comments (* ... *) within the term language are legacy
     1.8 +and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
     1.9 +instead.
    1.10 +
    1.11  * The "op <infix-op>" syntax for infix operators has been replaced by
    1.12  "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
    1.13  be a space between the "*" and the corresponding parenthesis.