# HG changeset patch
# User wenzelm
# Date 1287345270 -3600
# Node ID 78e6ec83762ac96962d5d050455b7b2e1d7d4526
# Parent  b8d89db3e238420866aaac0b245d6d83c3e19397
more on "Integers";

diff -r b8d89db3e238 -r 78e6ec83762a doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Oct 17 20:25:36 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Oct 17 20:54:30 2010 +0100
@@ -485,6 +485,35 @@
 *}
 
 
+subsection {* Integers *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type int} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML_type int} always 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
+  SML/NJ).
+
+  Literal integers in ML text (e.g.\ @{ML
+  123456789012345678901234567890}) are forced to be of this one true
+  integer type --- overloading of SML97 is disabled.
+
+  Structure @{ML_struct IntInf} of SML97 is obsolete, always use
+  @{ML_struct Int}.  Structure @{ML_struct Integer} in @{"file"
+  "~~/src/Pure/General/integer.ML"} provides some additional
+  operations.
+
+  \end{description}
+*}
+
+
 subsection {* Options *}
 
 text %mlref {*