# HG changeset patch
# User kleing
# Date 1066194223 -7200
# Node ID 9590df3c5f2a01ce8c5fe6991ea9ca72e972267d
# Parent  f6b6b2c55141f2bc2f2c103f907f5d2a0a6d5abf
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
conflict with locale subscript syntax)

diff -r f6b6b2c55141 -r 9590df3c5f2a NEWS
--- a/NEWS	Wed Oct 15 01:58:41 2003 +0200
+++ b/NEWS	Wed Oct 15 07:03:43 2003 +0200
@@ -17,9 +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: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
+  allowed in identifiers. Similar to greek letters \<^isub> is now considered 
+  a normal (but invisible) letter. For multiple letter subscripts repeat 
+  \<^isub> like this: x\<^isub>1\<^isub>2. 
 
 * Pure: Using the functions Theory.add_finals or Theory.add_finals_i
   or the new Isar command "finalconsts", it is now possible to
diff -r f6b6b2c55141 -r 9590df3c5f2a lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Oct 15 01:58:41 2003 +0200
+++ b/lib/texinputs/isabelle.sty	Wed Oct 15 07:03:43 2003 +0200
@@ -24,6 +24,8 @@
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r f6b6b2c55141 -r 9590df3c5f2a src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Oct 15 01:58:41 2003 +0200
+++ b/src/Pure/General/symbol.ML	Wed Oct 15 07:03:43 2003 +0200
@@ -110,7 +110,7 @@
 
     val bbb_letters = ["bool","complex","nat","rat","real","int"]
 
-    val control_letters = ["^sub"]
+    val control_letters = ["^isub", "^isup"]
  
     val pre_letters =
 	cal_letters   @