NEWS
changeset 14234 9590df3c5f2a
parent 14233 f6b6b2c55141
child 14237 a486123e24a5
     1.1 --- a/NEWS	Wed Oct 15 01:58:41 2003 +0200
     1.2 +++ b/NEWS	Wed Oct 15 07:03:43 2003 +0200
     1.3 @@ -17,9 +17,10 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 -* Pure: single letter subscripts (\<^sub>l) are now allowed in identifiers.
     1.8 -  Similar to greek letters \<^sub> is now considered a normal letter. 
     1.9 -	For multiple letter subscripts repeat \<^sub> like this: i\<^sub>1\<^sub>2. 
    1.10 +* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    1.11 +  allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    1.12 +  a normal (but invisible) letter. For multiple letter subscripts repeat 
    1.13 +  \<^isub> like this: x\<^isub>1\<^isub>2. 
    1.14  
    1.15  * Pure: Using the functions Theory.add_finals or Theory.add_finals_i
    1.16    or the new Isar command "finalconsts", it is now possible to