--- 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