--- a/NEWS Thu Feb 21 09:15:06 2019 +0000
+++ b/NEWS Thu Feb 21 09:15:06 2019 +0000
@@ -88,17 +88,18 @@
*** HOL ***
* Formal Laurent series and overhaul of Formal power series
-in HOL-Computational_Algebra
-
-* Exponentiation by squaring in HOL-Library; used for computing powers
-in monoid_mult and modular exponentiation in HOL-Number_Theory
-
-* more material on residue rings in HOL-Number_Theory:
-Carmichael's function, primitive roots, more properties for "ord"
-
-* the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
+in session HOL-Computational_Algebra.
+
+* Exponentiation by squaring in session HOL-Library; used for computing
+powers in class monoid_mult and modular exponentiation in session
+HOL-Number_Theory.
+
+* More material on residue rings in session HOL-Number_Theory:
+Carmichael's function, primitive roots, more properties for "ord".
+
+* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
(not the corresponding binding operators) now have the same precedence
-as any other prefix function symbol.
+as any other prefix function symbol. Minor INCOMPATIBILITY.
* Slightly more conventional naming schema in structure Inductive.
Minor INCOMPATIBILITY.