# HG changeset patch
# User haftmann
# Date 1253253266 -7200
# Node ID 1b3b0cc604ce7cb27d0e6220b1c4c7788cbd55ec
# Parent  979c274089a504c09ab42e3afa03000721c2c641
tuned NEWS, added CONTRIBUTORS

diff -r 979c274089a5 -r 1b3b0cc604ce CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Sep 17 19:13:22 2009 +0200
+++ b/CONTRIBUTORS	Fri Sep 18 07:54:26 2009 +0200
@@ -7,6 +7,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* September 2009: Florian Haftmann, TUM
+  Refinement of Sets and Lattices
+
+* July 2009: Jeremy Avigad and Amine Chaieb
+  New number theory
+
 * July 2009: Philipp Meyer, TUM
   HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
 
diff -r 979c274089a5 -r 1b3b0cc604ce NEWS
--- a/NEWS	Thu Sep 17 19:13:22 2009 +0200
+++ b/NEWS	Fri Sep 18 07:54:26 2009 +0200
@@ -19,14 +19,28 @@
 *** HOL ***
 
 * Reorganization of number theory:
-  * former session NumberTheory now named Old_Number_Theory; former session NewNumberTheory
-    named NumberTheory;
-  * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
+  * former session NumberTheory now named Old_Number_Theory
+  * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
   * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
   * moved theory Pocklington from Library/ to Old_Number_Theory/;
   * removed various references to Old_Number_Theory from HOL distribution.
 INCOMPATIBILITY.
 
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
+
+* Split off prime number ingredients from theory GCD
+to theory Number_Theory/Primes;
+
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
 * New testing tool "Mirabelle" for automated (proof) tools. Applies
 several tools and tactics like sledgehammer, metis, or quickcheck, to
 every proof step in a theory. To be used in batch mode via the
@@ -47,16 +61,15 @@
     etc.
   INCOMPATIBILITY.
 
-* New class "boolean_algebra".
-
 * Refinements to lattice classes and sets:
   - less default intro/elim rules in locale variant, more default
     intro/elim rules in class variant: more uniformity
   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
   - renamed ACI to inf_sup_aci
+  - new class "boolean_algebra"
   - class "complete_lattice" moved to separate theory "complete_lattice";
-    corresponding constants (and abbreviations) renamed:
+    corresponding constants (and abbreviations) renamed and with authentic syntax:
     Set.Inf ~>      Complete_Lattice.Inf
     Set.Sup ~>      Complete_Lattice.Sup
     Set.INFI ~>     Complete_Lattice.INFI
@@ -68,22 +81,18 @@
   - more convenient names for set intersection and union:
     Set.Int ~>  Set.inter
     Set.Un ~>   Set.union
+  - authentic syntax for
+    Set.Pow
+    Set.image
   - mere abbreviations:
     Set.empty               (for bot)
     Set.UNIV                (for top)
     Complete_Lattice.Inter  (for Inf)
     Complete_Lattice.Union  (for Sup)
+  - object-logic definitions as far as appropriate
 
   INCOMPATIBILITY.
 
-* Class semiring_div requires superclass no_zero_divisors and proof of
-div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
-div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
-generalized to class semiring_div, subsuming former theorems
-zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
-zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
-INCOMPATIBILITY.
-
 * Power operations on relations and functions are now one dedicate
 constant "compow" with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
@@ -96,10 +105,6 @@
 this.  Fix using O_assoc[symmetric].  The same applies to the curried
 version "R OO S".
 
-* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
-of finite and infinite sets. It is shown that they form a complete
-lattice.
-
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; see Predicate.thy for an example.
 
@@ -110,10 +115,6 @@
 default generators are provided for all suitable HOL types, records
 and datatypes.
 
-* Constants Set.Pow and Set.image now with authentic syntax;
-object-logic definitions Set.Pow_def and Set.image_def.
-INCOMPATIBILITY.
-
 * Renamed theorems:
 Suc_eq_add_numeral_1 -> Suc_eq_plus1
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
@@ -138,9 +139,6 @@
 
 INCOMPATIBILITY.
 
-* NewNumberTheory: Jeremy Avigad's new version of part of
-NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
-
 * Discontinued abbreviation "arbitrary" of constant
 "undefined". INCOMPATIBILITY, use "undefined" directly.