# HG changeset patch
# User wenzelm
# Date 1376825131 -7200
# Node ID f4811f3628dc256ec85466b884645c7e44fafdc8
# Parent  ce067c13d8e588293795b473446775e299ff5412
updated identifier syntax;

diff -r ce067c13d8e5 -r f4811f3628dc src/Doc/IsarRef/Outer_Syntax.thy
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Sat Aug 17 22:58:48 2013 +0200
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Sun Aug 18 13:25:31 2013 +0200
@@ -137,7 +137,7 @@
 
   \begin{center}
   \begin{supertabular}{rcl}
-    @{syntax_def ident} & = & @{text "letter quasiletter\<^sup>*"} \\
+    @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
     @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
     @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
     @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
@@ -150,7 +150,7 @@
     @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
 
     @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
-          &   & @{verbatim "\<^sub>"}@{text "  |  "}@{verbatim "\<^sup>"} \\
+    @{text subscript} & = & @{verbatim "\<^sub>"} \\
     @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
     @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
     @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\