NEWS
changeset 67446 1f4d167b6ac9
parent 67433 e0c0c1f0e3e7
child 67448 dbb1f02e667d
     1.1 --- a/NEWS	Tue Jan 16 09:58:17 2018 +0100
     1.2 +++ b/NEWS	Tue Jan 16 11:27:52 2018 +0100
     1.3 @@ -9,6 +9,11 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Marginal comments need to be written exclusively in the new-style form
     1.8 +"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
     1.9 +supported. INCOMPATIBILITY, use the command-line tool "isabelle
    1.10 +update_comments" to update existing theory files.
    1.11 +
    1.12  * The "op <infix-op>" syntax for infix operators has been replaced by
    1.13  "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
    1.14  be a space between the "*" and the corresponding parenthesis.