# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1555245146 -3600
# Node ID 1f163f772da30eabf89b288fdda46f59a82a1e45
# Parent  6152339771557d64222ee866bc8a393bc01fd1d3
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)

diff -r 615233977155 -r 1f163f772da3 CONTRIBUTORS
--- a/CONTRIBUTORS	Sun Apr 14 12:00:17 2019 +0100
+++ b/CONTRIBUTORS	Sun Apr 14 13:32:26 2019 +0100
@@ -6,6 +6,12 @@
 Contributions to Isabelle2019
 -----------------------------
 
+* April 2019: LC Paulson
+  Homology and supporting lemmas on topology and group theory
+
+* April 2019: Paulo de Vilhena and Martin Baillon
+  Group theory developments towards proving algebraic closure
+
 * February/March 2019: Makarius Wenzel
   Stateless management of export artifacts in the Isabelle/HOL code generator.
 
diff -r 615233977155 -r 1f163f772da3 NEWS
--- a/NEWS	Sun Apr 14 12:00:17 2019 +0100
+++ b/NEWS	Sun Apr 14 13:32:26 2019 +0100
@@ -268,8 +268,8 @@
 * Session HOL-Analysis: Better organization and much more material
 at the level of abstract topological spaces.
 
-* Session HOL-Algebra: Much more material on group theory, mostly ported
-from HOL Light.
+* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
+proofs towards algebraic closure by de Vilhena and Baillon.
 
 * Session HOL-SPARK: .prv files are no longer written to the
 file-system, but exported to the session database. Results may be