Subject: Announcing Isabelle2007 To: isabelle-users@cl.cam.ac.uk Isabelle2007 is finally available. This release introduces fundamental changes over Isabelle2005, see the NEWS file in the distribution for more details. Numerous existing concepts have been generalized and re-implemented based on novel system architecture. New theories and proof tools have been added (mostly for HOL). The main highlights are: * Fully featured support for nominal datatypes (binding structures) due to the HOL-Nominal logic. * General local theory infrastructure for specifications depending on parameters and assumptions (e.g. from locales, classes). * New basic specification elements 'definition', 'axiomatization', 'abbreviation', 'notation'. * New version of 'inductive' package for inductive predicates; separate variant 'inductive_set'. * New 'function' package for general recursive function definitions. * New 'class' package combination of axclass + locale interpretation. * Various improvements in locale infrastructure (interpretation etc.) * Various improvements of Isar language elements and related proof tools. * Built-in Metis prover, external linkup for automated provers, and 'sledghammer' command for automated proof synthesis. * Second generation code-generator for a subset of HOL, targeting SML, Haskell, and OCaml. * Improved support for arbitrary ML operations depending on the logical context. * Parallel loading of theories based on native multicore support in Poly/ML 5.1. You may get Isabelle2007 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/