NEWS
changeset 69506 7d59af98af29
parent 69470 c8c3285f1294
child 69546 27dae626822b
child 69568 de09a7261120
     1.1 --- a/NEWS	Wed Dec 26 16:25:20 2018 +0100
     1.2 +++ b/NEWS	Wed Dec 26 20:57:23 2018 +0100
     1.3 @@ -9,6 +9,10 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Old-style {* verbatim *} tokens are explicitly marked as legacy
     1.8 +feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
     1.9 +via "isabelle update_cartouches -t" (available since Isabelle2015).
    1.10 +
    1.11  * The font family "Isabelle DejaVu" is systematically derived from the
    1.12  existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
    1.13  and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".