NEWS
changeset 14561 c53396af770e
parent 14556 c5078f6c99a9
child 14572 1408d312d3a9
     1.1 --- a/NEWS	Wed Apr 14 11:44:57 2004 +0200
     1.2 +++ b/NEWS	Wed Apr 14 12:19:16 2004 +0200
     1.3 @@ -32,13 +32,10 @@
     1.4    PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
     1.5    new control characters are not identifier parts.
     1.6  
     1.7 -* Pure: Control-symbols of the form \<^raw...> will literally print the
     1.8 +* Pure: Control-symbols of the form \<^raw:...> will literally print the
     1.9    content of ... to the latex file instead of \isacntrl... . The ... 
    1.10    accepts all printable characters excluding the end bracket >.
    1.11  
    1.12 -* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
    1.13 -  longer accepted by the scanner.
    1.14 -
    1.15  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.16    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.17    declare constants "final", which prevents their being given a definition