--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Nov 20 00:53:26 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Nov 20 01:07:16 2010 +0100
@@ -1188,13 +1188,14 @@
\end{description}
\paragraph{Historical note.} In the original SML90 standard the
- primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of
- singleton strings as in Isabelle/ML today. When SML97 came out,
- Isabelle did not adopt its slightly anachronistic 8-bit characters,
- but the idea of exploding a string into a list of small strings was
- extended to ``symbols'' as explained above. Thus Isabelle sources
- can refer to an infinite store of user-defined symbols, without
- having to worry about the multitude of Unicode encodings.%
+ primitive ML type \verb|char| did not exists, and the \verb|explode: string -> string list| operation would produce a list of
+ singleton strings as does \verb|raw_explode: string -> string list|
+ in Isabelle/ML today. When SML97 came out, Isabelle did not adopt
+ its slightly anachronistic 8-bit characters, but the idea of
+ exploding a string into a list of small strings was extended to
+ ``symbols'' as explained above. Thus Isabelle sources can refer to
+ an infinite store of user-defined symbols, without having to worry
+ about the multitude of Unicode encodings.%
\end{isamarkuptext}%
\isamarkuptrue%
%