allow \<^sub> in identifiers
authorkleing
Wed Oct 15 01:58:41 2003 +0200 (2003-10-15)
changeset 14233f6b6b2c55141
parent 14232 ef550525c591
child 14234 9590df3c5f2a
allow \<^sub> in identifiers
NEWS
     1.1 --- a/NEWS	Wed Oct 15 01:52:47 2003 +0200
     1.2 +++ b/NEWS	Wed Oct 15 01:58:41 2003 +0200
     1.3 @@ -17,6 +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 +
    1.11  * Pure: Using the functions Theory.add_finals or Theory.add_finals_i
    1.12    or the new Isar command "finalconsts", it is now possible to
    1.13    make constants "final", thereby ensuring that they are not defined