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