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

author | wenzelm |

Mon, 23 Nov 2009 22:47:08 +0100 | |

changeset 33873 | e9120a7b2779 |

parent 33872 | 04c560b4ebc1 |

child 33874 | 1db5ca5eadf5 |

more tuning for release;

ANNOUNCE | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

--- a/ANNOUNCE Mon Nov 23 22:35:54 2009 +0100 +++ b/ANNOUNCE Mon Nov 23 22:47:08 2009 +0100 @@ -7,24 +7,35 @@ file in the distribution for more details. Some important changes are: -* Proof method "smt" for a combination of first-order logic with equality, -linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors. - -* Counterexample generator tool »nitpick« based on the Kodkod relational model finder. +* Isabelle tool "wwwfind" provides web interface for 'find_theorems' +on a given logic image. -* Predicate compiler turning inductive into (executable) equational specifications. - -* Refined number theory. - -* Various parts of multivariate analysis. +* HOL-SMT: proof method "smt" for a combination of first-order logic +with equality, linear and nonlinear (natural/integer/real) arithmetic, +and fixed-size bitvectors. * HOL-Boogie: an interactive prover back-end for Boogie and VCC. +* HOL: Counterexample generator tool Nitpick based on the Kodkod +relational model finder. + +* HOL: predicate compiler turning inductive into (executable) +equational specifications. + +* HOL: refined number theory. + +* HOL: various parts of multivariate analysis. + +* HOLCF: new definitional domain package. + * Revised tutorial on locales. -* New definitional domain package for HOLCF. +* Support for Poly/ML 5.3.0, with improved reporting of compiler +errors and run-time exceptions, including detailed source positions. -* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions. +* Parallel checking of nested Isar proofs, with improved scalability +up to 8 cores. + You may get Isabelle2009-1 from the following mirror sites:

--- a/NEWS Mon Nov 23 22:35:54 2009 +0100 +++ b/NEWS Mon Nov 23 22:47:08 2009 +0100 @@ -114,19 +114,17 @@ fixpoint theorem. * Reorganization of number theory, INCOMPATIBILITY: - - new number theory development for nat and int, in - theories Divides and GCD as well as in new session - Number_Theory - - some constants and facts now suffixed with _nat and - _int accordingly - - former session NumberTheory now named Old_Number_Theory, - including theories Legacy_GCD and Primes (prefer Number_Theory - if possible) + - new number theory development for nat and int, in theories Divides + and GCD as well as in new session Number_Theory + - some constants and facts now suffixed with _nat and _int + accordingly + - former session NumberTheory now named Old_Number_Theory, including + theories Legacy_GCD and Primes (prefer Number_Theory if possible) - moved theory Pocklington from src/HOL/Library to src/HOL/Old_Number_Theory -* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm -of finite and infinite sets. It is shown that they form a complete +* Theory GCD includes 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. * Class semiring_div requires superclass no_zero_divisors and proof of @@ -198,8 +196,6 @@ abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. INCOMPATIBILITY. --- - * Most rules produced by inductive and datatype package have mandatory prefixes. INCOMPATIBILITY. @@ -208,8 +204,9 @@ DERIV_intros assumes composition with an additional function and matches a variable to the derivative, which has to be solved by the Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative -of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac -should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY. +of most elementary terms. Former Maclauren.DERIV_tac and +Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros). +INCOMPATIBILITY. * Code generator attributes follow the usual underscore convention: code_unfold replaces code unfold @@ -274,7 +271,8 @@ * The 'fixrec' package now supports "bottom patterns". Bottom patterns can be used to generate strictness rules, or to make functions more strict (much like the bang-patterns supported by the -Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples. +Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for +examples. *** ML ***