summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 01 Oct 2007 21:08:26 +0200 | |

changeset 24801 | f53f6b08e13a |

parent 24800 | 3ab455b3d03b |

child 24802 | 6bd8ec8f3fc8 |

misc tuning and update;

--- a/NEWS Mon Oct 01 21:04:40 2007 +0200 +++ b/NEWS Mon Oct 01 21:08:26 2007 +0200 @@ -1,8 +1,8 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New in this Isabelle version ----------------------------- +New in Isabelle2007 +------------------- *** General *** @@ -1088,23 +1088,6 @@ is available in HOL/ex/ReflectionEx.thy -*** HOL-Algebra *** - -* Formalisation of ideals and the quotient construction over rings. - -* Order and lattice theory no longer based on records. -INCOMPATIBILITY. - -* Renamed lemmas least_carrier -> least_closed and greatest_carrier -> -greatest_closed. INCOMPATIBILITY. - -* Method algebra is now set up via an attribute. For examples see -Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations -of algebraic structures. - -* Renamed theory CRing to Ring. - - *** HOL-Complex *** * Hyperreal: Functions root and sqrt are now defined on negative real @@ -1161,6 +1144,30 @@ (ns)deriv <-- (ns)cderiv +*** HOL-Algebra *** + +* Formalisation of ideals and the quotient construction over rings. + +* Order and lattice theory no longer based on records. +INCOMPATIBILITY. + +* Renamed lemmas least_carrier -> least_closed and greatest_carrier -> +greatest_closed. INCOMPATIBILITY. + +* Method algebra is now set up via an attribute. For examples see +Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations +of algebraic structures. + +* Renamed theory CRing to Ring. + + +*** HOL-Nominal *** + +* Fully featured support for nominal datatypes (binding structures) +due to the HOL-Nominal logic. See HOL/Nominal, HOL/Nominal/Examples, +and http://isabelle.in.tum.de/nominal/download.html + + *** ML *** * ML basics: just one true type int, which coincides with IntInf.int @@ -1353,7 +1360,7 @@ operations, notably runtime compilation and evaluation of ML source code. -* Support for parall execution, using native multicore support of +* Support for parallel execution, using native multicore support of Poly/ML 5.1. The theory loader exploits parallelism when processing independent theories, according to the given theory header specifications. The maximum number of worker threads is specified via