diff -r 1a29ea173bf9 -r 0b7a0c1fdf7e src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon Jan 20 20:38:51 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Wed Jan 22 15:10:33 2014 +0100
@@ -631,18 +631,19 @@
     @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
-
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
+    @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
 
   The token categories @{syntax (inner) num_token}, @{syntax (inner)
   float_token}, @{syntax (inner) xnum_token}, @{syntax (inner)
-  str_token}, and @{syntax (inner) cartouche} are not used in Pure.
-  Object-logics may implement numerals and string literals by adding
-  appropriate syntax declarations, together with some translation
-  functions (e.g.\ see Isabelle/HOL).
+  str_token}, @{syntax (inner) string_token}, and @{syntax (inner)
+  cartouche} are not used in Pure. Object-logics may implement
+  numerals and string literals by adding appropriate syntax
+  declarations, together with some translation functions (e.g.\ see
+  @{file "~~/src/HOL/Tools/string_syntax.ML"}).
 
   The derived categories @{syntax_def (inner) num_const}, @{syntax_def
   (inner) float_const}, and @{syntax_def (inner) num_const} provide