# HG changeset patch
# User wenzelm
# Date 1555437614 -7200
# Node ID e79bbf86a984b4e92cdaff572e4a05f4599793d0
# Parent  b33f28c81ba9130db712a2d82a53464786001437
tuned for release;

diff -r b33f28c81ba9 -r e79bbf86a984 NEWS
--- 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