author wenzelm Mon Nov 23 22:47:08 2009 +0100 (2009-11-23) changeset 33873 e9120a7b2779 parent 33872 04c560b4ebc1 child 33874 1db5ca5eadf5
more tuning for release;
 ANNOUNCE file | annotate | diff | revisions NEWS file | annotate | diff | revisions
```     1.1 --- a/ANNOUNCE	Mon Nov 23 22:35:54 2009 +0100
1.2 +++ b/ANNOUNCE	Mon Nov 23 22:47:08 2009 +0100
1.3 @@ -7,24 +7,35 @@
1.4  file in the distribution for more details.  Some important changes
1.5  are:
1.6
1.7 -* Proof method "smt" for a combination of first-order logic with equality,
1.8 -linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
1.9 -
1.10 -* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
1.11 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
1.12 +on a given logic image.
1.13
1.14 -* Predicate compiler turning inductive into (executable) equational specifications.
1.15 -
1.16 -* Refined number theory.
1.17 -
1.18 -* Various parts of multivariate analysis.
1.19 +* HOL-SMT: proof method "smt" for a combination of first-order logic
1.20 +with equality, linear and nonlinear (natural/integer/real) arithmetic,
1.21 +and fixed-size bitvectors.
1.22
1.23  * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
1.24
1.25 +* HOL: Counterexample generator tool Nitpick based on the Kodkod
1.26 +relational model finder.
1.27 +
1.28 +* HOL: predicate compiler turning inductive into (executable)
1.29 +equational specifications.
1.30 +
1.31 +* HOL: refined number theory.
1.32 +
1.33 +* HOL: various parts of multivariate analysis.
1.34 +
1.35 +* HOLCF: new definitional domain package.
1.36 +
1.37  * Revised tutorial on locales.
1.38
1.39 -* New definitional domain package for HOLCF.
1.40 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
1.41 +errors and run-time exceptions, including detailed source positions.
1.42
1.43 -* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
1.44 +* Parallel checking of nested Isar proofs, with improved scalability
1.45 +up to 8 cores.
1.46 +
1.47
1.48  You may get Isabelle2009-1 from the following mirror sites:
1.49
```
```     2.1 --- a/NEWS	Mon Nov 23 22:35:54 2009 +0100
2.2 +++ b/NEWS	Mon Nov 23 22:47:08 2009 +0100
2.3 @@ -114,19 +114,17 @@
2.4  fixpoint theorem.
2.5
2.6  * Reorganization of number theory, INCOMPATIBILITY:
2.7 -  - new number theory development for nat and int, in
2.8 -    theories Divides and GCD as well as in new session
2.9 -    Number_Theory
2.10 -  - some constants and facts now suffixed with _nat and
2.11 -    _int accordingly
2.12 -  - former session NumberTheory now named Old_Number_Theory,
2.13 -    including theories Legacy_GCD and Primes (prefer Number_Theory
2.14 -    if possible)
2.15 +  - new number theory development for nat and int, in theories Divides
2.16 +    and GCD as well as in new session Number_Theory
2.17 +  - some constants and facts now suffixed with _nat and _int
2.18 +    accordingly
2.19 +  - former session NumberTheory now named Old_Number_Theory, including
2.20 +    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
2.21    - moved theory Pocklington from src/HOL/Library to
2.22      src/HOL/Old_Number_Theory
2.23
2.24 -* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
2.25 -of finite and infinite sets. It is shown that they form a complete
2.26 +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
2.27 +lcm of finite and infinite sets. It is shown that they form a complete
2.28  lattice.
2.29
2.30  * Class semiring_div requires superclass no_zero_divisors and proof of
2.31 @@ -198,8 +196,6 @@
2.32  abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
2.33  INCOMPATIBILITY.
2.34
2.35 ---
2.36 -
2.37  * Most rules produced by inductive and datatype package have mandatory
2.38  prefixes.  INCOMPATIBILITY.
2.39
2.40 @@ -208,8 +204,9 @@
2.41  DERIV_intros assumes composition with an additional function and
2.42  matches a variable to the derivative, which has to be solved by the
2.43  Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
2.44 -of most elementary terms.  Former Maclauren.DERIV_tac and Maclauren.deriv_tac
2.45 -should be replaced by (auto intro!: DERIV_intros).  INCOMPATIBILITY.
2.46 +of most elementary terms.  Former Maclauren.DERIV_tac and
2.47 +Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
2.48 +INCOMPATIBILITY.
2.49
2.50  * Code generator attributes follow the usual underscore convention:
2.51      code_unfold     replaces    code unfold
2.52 @@ -274,7 +271,8 @@
2.53  * The 'fixrec' package now supports "bottom patterns".  Bottom
2.54  patterns can be used to generate strictness rules, or to make
2.55  functions more strict (much like the bang-patterns supported by the
2.56 -Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for examples.
2.57 +Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
2.58 +examples.
2.59
2.60
2.61  *** ML ***
```