Gauss, UNITY, ZF
authorpaulson
Thu Mar 20 17:15:16 2003 +0100 (2003-03-20)
changeset 13872601514e63534
parent 13871 26e5f5e624f6
child 13873 f9f49a1ec0f2
Gauss, UNITY, ZF
NEWS
     1.1 --- a/NEWS	Thu Mar 20 15:58:25 2003 +0100
     1.2 +++ b/NEWS	Thu Mar 20 17:15:16 2003 +0100
     1.3 @@ -103,8 +103,6 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* GroupTheory: new, experimental summation operator for abelian groups.
     1.8 -
     1.9  * New tactic "trans_tac" and method "trans" instantiate
    1.10  Provers/linorder.ML for axclasses "order" and "linorder" (predicates
    1.11  "<=", "<" and "="). 
    1.12 @@ -142,17 +140,23 @@
    1.13  * induct over a !!-quantified statement (say !!x1..xn):
    1.14    each "case" automatically performs "fix x1 .. xn" with exactly those names.
    1.15  
    1.16 -* GroupTheory: converted to Isar theories, using locales with implicit structures;
    1.17 -
    1.18  * Real/HahnBanach: updated and adapted to locales;
    1.19  
    1.20 +* GroupTheory: converted to Isar theories, using locales with implicit
    1.21 +structures.  Also a new, experimental summation operator for abelian groups;
    1.22 +
    1.23 +* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
    1.24 +Kramer);
    1.25 +
    1.26 +* UNITY: added the Meier-Sanders theory of progress sets;
    1.27 +
    1.28  
    1.29  *** ZF ***
    1.30  
    1.31  * ZF/Constructible: consistency proof for AC (Gödel's constructible
    1.32  universe, etc.);
    1.33  
    1.34 -* Main ZF: many theories converted to new-style format;
    1.35 +* Main ZF: virtually all theories converted to new-style format;
    1.36  
    1.37  
    1.38  *** ML ***