# HG changeset patch
# User wenzelm
# Date 1464809091 -7200
# Node ID c7de5b311909f8aad60596250a6594417dad69d6
# Parent  7e8ef9ac315935c8ef27f2bceb23f2d74edd1517
more documentation;

diff -r 7e8ef9ac3159 -r c7de5b311909 NEWS
--- a/NEWS	Wed Jun 01 20:59:16 2016 +0200
+++ b/NEWS	Wed Jun 01 21:24:51 2016 +0200
@@ -348,10 +348,10 @@
 *** ML ***
 
 * Structure Rat for rational numbers is now an integral part of
-Isabelle/ML, with special notation @int/nat for numerals (an
-abbreviation for antiquotation @{Pure.rat int/nat}) and ML pretty
+Isabelle/ML, with special notation @int/nat or @int for numerals (an
+abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
 printing. Standard operations on type Rat.rat are provided via ad-hoc
-overloading of + - * / = < <= > >= <> ~ abs. INCOMPATIBILITY, need to
+overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
 use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
 superseded by General.Div.
 
diff -r 7e8ef9ac3159 -r c7de5b311909 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Jun 01 20:59:16 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Wed Jun 01 21:24:51 2016 +0200
@@ -1381,15 +1381,31 @@
   practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
   32-bit Poly/ML, and much higher for 64-bit systems.\<close>
 
-  Literal integers in ML text are forced to be of this one true integer type
-  --- adhoc overloading of SML97 is disabled.
-
   Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
   @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
   "~~/src/Pure/General/integer.ML"} provides some additional operations.
 \<close>
 
 
+subsection \<open>Rational numbers\<close>
+
+text %mlref \<open>
+  \begin{mldecls}
+  @{index_ML_type Rat.rat} \\
+  \end{mldecls}
+
+  \<^descr> Type @{ML_type Rat.rat} represents rational numbers, based on the
+  unbounded integers of Poly/ML.
+
+  Literal rationals may be written with special antiquotation syntax
+  \<^verbatim>\<open>@\<close>\<open>int\<close>\<^verbatim>\<open>/\<close>\<open>nat\<close> or \<^verbatim>\<open>@\<close>\<open>int\<close> (without any white space). For example
+  \<^verbatim>\<open>@~1/4\<close> or \<^verbatim>\<open>@10\<close>. The ML toplevel pretty printer uses the same format.
+
+  Standard operations are provided via ad-hoc overloading of \<^verbatim>\<open>+\<close>, \<^verbatim>\<open>-\<close>, \<^verbatim>\<open>*\<close>,
+  \<^verbatim>\<open>/\<close>, etc.
+\<close>
+
+
 subsection \<open>Time\<close>
 
 text %mlref \<open>