more tuning for release;
authorwenzelm
Mon Nov 23 22:47:08 2009 +0100 (2009-11-23)
changeset 33873e9120a7b2779
parent 33872 04c560b4ebc1
child 33874 1db5ca5eadf5
more tuning for release;
ANNOUNCE
NEWS
     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 ***