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