\<^bsub> .. \<^esub>
authorkleing
Mon Dec 29 06:49:26 2003 +0100 (2003-12-29)
changeset 1433314f29eb097a3
parent 14332 fd3535af90ab
child 14334 6137d24eef79
\<^bsub> .. \<^esub>
NEWS
     1.1 --- a/NEWS	Mon Dec 29 06:07:44 2003 +0100
     1.2 +++ b/NEWS	Mon Dec 29 06:49:26 2003 +0100
     1.3 @@ -24,6 +24,11 @@
     1.4    a normal (but invisible) letter. For multiple letter subscripts repeat 
     1.5    \<^isub> like this: x\<^isub>1\<^isub>2. 
     1.6  
     1.7 +* Pure: There are now sub-/superscripts that can span more than one
     1.8 +  character. Text between \<^bsub> and \<^esub> is set in subscript in
     1.9 +  PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
    1.10 +  new control characters are not identifier parts.
    1.11 +
    1.12  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.13    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.14    declare constants "final", which prevents their being given a definition