diff -r 529464cffbfe -r c53396af770e NEWS
--- a/NEWS	Wed Apr 14 11:44:57 2004 +0200
+++ b/NEWS	Wed Apr 14 12:19:16 2004 +0200
@@ -32,13 +32,10 @@
   PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
   new control characters are not identifier parts.
 
-* Pure: Control-symbols of the form \<^raw...> will literally print the
+* Pure: Control-symbols of the form \<^raw:...> will literally print the
   content of ... to the latex file instead of \isacntrl... . The ... 
   accepts all printable characters excluding the end bracket >.
 
-* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
-  longer accepted by the scanner.
-
 * Pure: Using new Isar command "finalconsts" (or the ML functions
   Theory.add_finals or Theory.add_finals_i) it is now possible to
   declare constants "final", which prevents their being given a definition