NEWS
changeset 14361 ad2f5da643b4
parent 14333 14f29eb097a3
child 14375 a545da363b23
     1.1 --- a/NEWS	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/NEWS	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -29,6 +29,13 @@
     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 +  content of ... to the latex file instead of \isacntrl... . The ... 
     1.9 +  accepts all printable characters excluding the end bracket >.
    1.10 +
    1.11 +* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
    1.12 +  longer accepted by the scanner.
    1.13 +
    1.14  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.15    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.16    declare constants "final", which prevents their being given a definition