--- a/NEWS Tue Apr 16 19:42:56 2019 +0200
+++ b/NEWS Tue Apr 16 20:00:14 2019 +0200
@@ -249,8 +249,8 @@
precedence as any other prefix function symbol.
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
-of the bundle cardinal_syntax (available in Main).
-Minor INCOMPATIBILITY.
+of the bundle cardinal_syntax (available in theory Main). Minor
+INCOMPATIBILITY.
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
used for computing powers in class "monoid_mult" and modular
@@ -262,15 +262,16 @@
* Session HOL-Number_Theory: More material on residue rings in
Carmichael's function, primitive roots, more properties for "ord".
-* Session HOL-Homology: New, a port of HOL Light's homology library,
-with new proofs of "invariance of domain" and related results.
-
* Session HOL-Analysis: Better organization and much more material
at the level of abstract topological spaces.
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
proofs towards algebraic closure by de Vilhena and Baillon.
+* Session HOL-Homology has been added. It is a port of HOL Light's
+homology library, with new proofs of "invariance of domain" and related
+results.
+
* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved via "isabelle build -e HOL-SPARK-Examples" on the