\<^bsub> .. \<^esub>

--- a/NEWS	Mon Dec 29 06:07:44 2003 +0100
+++ b/NEWS	Mon Dec 29 06:49:26 2003 +0100
@@ -24,6 +24,11 @@
   a normal (but invisible) letter. For multiple letter subscripts repeat 
   \<^isub> like this: x\<^isub>1\<^isub>2. 
 
+* Pure: There are now sub-/superscripts that can span more than one
+  character. Text between \<^bsub> and \<^esub> is set in subscript in
+  PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
+  new control characters are not identifier parts.
+
 * 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