# HG changeset patch
# User kleing
# Date 1066175921 -7200
# Node ID f6b6b2c55141f2bc2f2c103f907f5d2a0a6d5abf
# Parent  ef550525c591bd8d9ee823147dd0834a58e2cf70
allow \<^sub> in identifiers

diff -r ef550525c591 -r f6b6b2c55141 NEWS
--- a/NEWS	Wed Oct 15 01:52:47 2003 +0200
+++ b/NEWS	Wed Oct 15 01:58:41 2003 +0200
@@ -17,6 +17,10 @@
   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
   existing theory and ML files.
 
+* Pure: single letter subscripts (\<^sub>l) are now allowed in identifiers.
+  Similar to greek letters \<^sub> is now considered a normal letter. 
+	For multiple letter subscripts repeat \<^sub> like this: i\<^sub>1\<^sub>2. 
+
 * Pure: Using the functions Theory.add_finals or Theory.add_finals_i
   or the new Isar command "finalconsts", it is now possible to
   make constants "final", thereby ensuring that they are not defined