--- 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 ***