summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

ANNOUNCE

changeset 33873 | e9120a7b2779 |

parent 33866 | 34e45b2afe43 |

child 33881 | d8958955ecb5 |

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