--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 18 15:35:20 2010 +0100
@@ -494,8 +494,9 @@
\begin{description}
- \item @{ML_type char} is not used. The smallest textual unit in
- Isabelle is a ``symbol'' (see \secref{sec:symbols}).
+ \item Type @{ML_type char} is \emph{not} used. The smallest textual
+ unit in Isabelle is represented a ``symbol'' (see
+ \secref{sec:symbols}).
\end{description}
*}
@@ -510,8 +511,8 @@
\begin{description}
- \item @{ML_type int} represents regular mathematical integers, which
- are \emph{unbounded}. Overflow never happens in
+ \item Type @{ML_type int} represents regular mathematical integers,
+ which are \emph{unbounded}. Overflow never happens in
practice.\footnote{The size limit for integer bit patterns in memory
is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.}
This works uniformly for all supported ML platforms (Poly/ML and