summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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