| changeset 32130 | 2a0645733185 |
| parent 32079 | 5dc52b199815 |
| child 32131 | 7913823f14e3 |
--- a/NEWS Wed Jul 22 08:05:33 2009 +0200 +++ b/NEWS Wed Jul 22 10:49:26 2009 +0200 @@ -49,6 +49,9 @@ multiplicative monoids retains syntax "^" and is now defined generic in class power. INCOMPATIBILITY. +* 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.