# HG changeset patch # User paulson # Date 1048176916 -3600 # Node ID 601514e635340ad6196823723e0e009c502aadd6 # Parent 26e5f5e624f6eb0231ee89a4dd4d5ce72de4dd89 Gauss, UNITY, ZF diff -r 26e5f5e624f6 -r 601514e63534 NEWS --- a/NEWS Thu Mar 20 15:58:25 2003 +0100 +++ b/NEWS Thu Mar 20 17:15:16 2003 +0100 @@ -103,8 +103,6 @@ *** HOL *** -* GroupTheory: new, experimental summation operator for abelian groups. - * New tactic "trans_tac" and method "trans" instantiate Provers/linorder.ML for axclasses "order" and "linorder" (predicates "<=", "<" and "="). @@ -142,17 +140,23 @@ * induct over a !!-quantified statement (say !!x1..xn): each "case" automatically performs "fix x1 .. xn" with exactly those names. -* GroupTheory: converted to Isar theories, using locales with implicit structures; - * Real/HahnBanach: updated and adapted to locales; +* GroupTheory: converted to Isar theories, using locales with implicit +structures. Also a new, experimental summation operator for abelian groups; + +* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and +Kramer); + +* UNITY: added the Meier-Sanders theory of progress sets; + *** ZF *** * ZF/Constructible: consistency proof for AC (Gödel's constructible universe, etc.); -* Main ZF: many theories converted to new-style format; +* Main ZF: virtually all theories converted to new-style format; *** ML ***