--- a/NEWS Sat Jun 04 16:10:44 2016 +0200
+++ b/NEWS Sat Jun 04 16:23:42 2016 +0200
@@ -348,9 +348,10 @@
*** ML ***
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
-(notably for big integers). Subtle change of semantics: Integer.gcd and
-Integer.lcm both normalize the sign, results are never negative. This
-coincides with the definitions in HOL/GCD.thy. INCOMPATIBILITY.
+library (notably for big integers). Subtle change of semantics:
+Integer.gcd and Integer.lcm both normalize the sign, results are never
+negative. This coincides with the definitions in HOL/GCD.thy.
+INCOMPATIBILITY.
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an