Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
authorpaulson <lp15@cam.ac.uk>
Sun Apr 14 13:32:26 2019 +0100 (5 months ago)
changeset 701641f163f772da3
parent 70163 615233977155
child 70165 48e8bbeef7d3
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Sun Apr 14 12:00:17 2019 +0100
     1.2 +++ b/CONTRIBUTORS	Sun Apr 14 13:32:26 2019 +0100
     1.3 @@ -6,6 +6,12 @@
     1.4  Contributions to Isabelle2019
     1.5  -----------------------------
     1.6  
     1.7 +* April 2019: LC Paulson
     1.8 +  Homology and supporting lemmas on topology and group theory
     1.9 +
    1.10 +* April 2019: Paulo de Vilhena and Martin Baillon
    1.11 +  Group theory developments towards proving algebraic closure
    1.12 +
    1.13  * February/March 2019: Makarius Wenzel
    1.14    Stateless management of export artifacts in the Isabelle/HOL code generator.
    1.15  
     2.1 --- a/NEWS	Sun Apr 14 12:00:17 2019 +0100
     2.2 +++ b/NEWS	Sun Apr 14 13:32:26 2019 +0100
     2.3 @@ -268,8 +268,8 @@
     2.4  * Session HOL-Analysis: Better organization and much more material
     2.5  at the level of abstract topological spaces.
     2.6  
     2.7 -* Session HOL-Algebra: Much more material on group theory, mostly ported
     2.8 -from HOL Light.
     2.9 +* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
    2.10 +proofs towards algebraic closure by de Vilhena and Baillon.
    2.11  
    2.12  * Session HOL-SPARK: .prv files are no longer written to the
    2.13  file-system, but exported to the session database. Results may be