1.1 --- a/CONTRIBUTORS	Thu Sep 17 19:13:22 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Sep 18 07:54:26 2009 +0200
     1.3 @@ -7,6 +7,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2009: Florian Haftmann, TUM
     1.8 +  Refinement of Sets and Lattices
     1.9 +
    1.10 +* July 2009: Jeremy Avigad and Amine Chaieb
    1.11 +  New number theory
    1.12 +
    1.13  * July 2009: Philipp Meyer, TUM
    1.14    HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
    1.15  

     2.1 --- a/NEWS	Thu Sep 17 19:13:22 2009 +0200
     2.2 +++ b/NEWS	Fri Sep 18 07:54:26 2009 +0200
     2.3 @@ -19,14 +19,28 @@
     2.4  *** HOL ***
     2.5  
     2.6  * Reorganization of number theory:
     2.7 -  * former session NumberTheory now named Old_Number_Theory; former session NewNumberTheory
     2.8 -    named NumberTheory;
     2.9 -  * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
    2.10 +  * former session NumberTheory now named Old_Number_Theory
    2.11 +  * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
    2.12    * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
    2.13    * moved theory Pocklington from Library/ to Old_Number_Theory/;
    2.14    * removed various references to Old_Number_Theory from HOL distribution.
    2.15  INCOMPATIBILITY.
    2.16  
    2.17 +* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
    2.18 +of finite and infinite sets. It is shown that they form a complete
    2.19 +lattice.
    2.20 +
    2.21 +* Split off prime number ingredients from theory GCD
    2.22 +to theory Number_Theory/Primes;
    2.23 +
    2.24 +* Class semiring_div requires superclass no_zero_divisors and proof of
    2.25 +div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    2.26 +div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
    2.27 +generalized to class semiring_div, subsuming former theorems
    2.28 +zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
    2.29 +zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
    2.30 +INCOMPATIBILITY.
    2.31 +
    2.32  * New testing tool "Mirabelle" for automated (proof) tools. Applies
    2.33  several tools and tactics like sledgehammer, metis, or quickcheck, to
    2.34  every proof step in a theory. To be used in batch mode via the
    2.35 @@ -47,16 +61,15 @@
    2.36      etc.
    2.37    INCOMPATIBILITY.
    2.38  
    2.39 -* New class "boolean_algebra".
    2.40 -
    2.41  * Refinements to lattice classes and sets:
    2.42    - less default intro/elim rules in locale variant, more default
    2.43      intro/elim rules in class variant: more uniformity
    2.44    - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
    2.45    - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
    2.46    - renamed ACI to inf_sup_aci
    2.47 +  - new class "boolean_algebra"
    2.48    - class "complete_lattice" moved to separate theory "complete_lattice";
    2.49 -    corresponding constants (and abbreviations) renamed:
    2.50 +    corresponding constants (and abbreviations) renamed and with authentic syntax:
    2.51      Set.Inf ~>      Complete_Lattice.Inf
    2.52      Set.Sup ~>      Complete_Lattice.Sup
    2.53      Set.INFI ~>     Complete_Lattice.INFI
    2.54 @@ -68,22 +81,18 @@
    2.55    - more convenient names for set intersection and union:
    2.56      Set.Int ~>  Set.inter
    2.57      Set.Un ~>   Set.union
    2.58 +  - authentic syntax for
    2.59 +    Set.Pow
    2.60 +    Set.image
    2.61    - mere abbreviations:
    2.62      Set.empty               (for bot)
    2.63      Set.UNIV                (for top)
    2.64      Complete_Lattice.Inter  (for Inf)
    2.65      Complete_Lattice.Union  (for Sup)
    2.66 +  - object-logic definitions as far as appropriate
    2.67  
    2.68    INCOMPATIBILITY.
    2.69  
    2.70 -* Class semiring_div requires superclass no_zero_divisors and proof of
    2.71 -div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    2.72 -div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
    2.73 -generalized to class semiring_div, subsuming former theorems
    2.74 -zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
    2.75 -zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
    2.76 -INCOMPATIBILITY.
    2.77 -
    2.78  * Power operations on relations and functions are now one dedicate
    2.79  constant "compow" with infix syntax "^^".  Power operations on
    2.80  multiplicative monoids retains syntax "^" and is now defined generic
    2.81 @@ -96,10 +105,6 @@
    2.82  this.  Fix using O_assoc[symmetric].  The same applies to the curried
    2.83  version "R OO S".
    2.84  
    2.85 -* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
    2.86 -of finite and infinite sets. It is shown that they form a complete
    2.87 -lattice.
    2.88 -
    2.89  * ML antiquotation @{code_datatype} inserts definition of a datatype
    2.90  generated by the code generator; see Predicate.thy for an example.
    2.91  
    2.92 @@ -110,10 +115,6 @@
    2.93  default generators are provided for all suitable HOL types, records
    2.94  and datatypes.
    2.95  
    2.96 -* Constants Set.Pow and Set.image now with authentic syntax;
    2.97 -object-logic definitions Set.Pow_def and Set.image_def.
    2.98 -INCOMPATIBILITY.
    2.99 -
   2.100  * Renamed theorems:
   2.101  Suc_eq_add_numeral_1 -> Suc_eq_plus1
   2.102  Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
   2.103 @@ -138,9 +139,6 @@
   2.104  
   2.105  INCOMPATIBILITY.
   2.106  
   2.107 -* NewNumberTheory: Jeremy Avigad's new version of part of
   2.108 -NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
   2.109 -
   2.110  * Discontinued abbreviation "arbitrary" of constant
   2.111  "undefined". INCOMPATIBILITY, use "undefined" directly.
   2.112