NEWS
changeset 32130 2a0645733185
parent 32079 5dc52b199815
child 32131 7913823f14e3
     1.1 --- a/NEWS	Wed Jul 22 08:05:33 2009 +0200
     1.2 +++ b/NEWS	Wed Jul 22 10:49:26 2009 +0200
     1.3 @@ -49,6 +49,9 @@
     1.4  multiplicative monoids retains syntax "^" and is now defined generic
     1.5  in class power.  INCOMPATIBILITY.
     1.6  
     1.7 +* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
     1.8 +infinite sets. It is shown that they form a complete lattice.
     1.9 +
    1.10  * ML antiquotation @{code_datatype} inserts definition of a datatype
    1.11  generated by the code generator; see Predicate.thy for an example.
    1.12