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;

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