src/Doc/IsarRef/Outer_Syntax.thy
changeset 53015 a1119cf551e8
parent 51062 d5fd24f73555
child 53059 f4811f3628dc
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -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 "\<^isub>"}@{text "  |  "}@{verbatim "\<^isup>"} \\
+          &   & @{verbatim "\<^sub>"}@{text "  |  "}@{verbatim "\<^sup>"} \\
     @{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"} \\