1 Subject: Announcing Isabelle2009
2 To: isabelle-users@cl.cam.ac.uk
4 Isabelle2009 is now available.
6 This release significantly improves upon Isabelle2008, see the NEWS
7 file in the distribution for more details. Some important changes
10 * Complete re-implementation of locales, with proper support for local
11 syntax, and more robust interpretation mechanism.
13 * New 'find_consts' and 'find_theorems' facilities, together with
14 "auto solve" feature of toplevel goal statements.
16 * HOL: reorganization of main logic images.
18 * HOL: improved implementation of Sledgehammer, based on generic ATP
19 manager; support for remote ATPs.
21 * HOL: numerous library improvements.
23 * Updated and extended versions of main reference manuals.
25 * Simplified arrangement of Isabelle startup scripts and settings
28 * Simplified internal programming interfaces for all Isar language
31 * General high-level support for concurrent ML programming.
33 * Parallel proof checking within Isar theories.
36 You may get Isabelle2009 from the following mirror sites:
38 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
39 Munich (Germany) http://isabelle.in.tum.de/
40 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/