Subject: Announcing Isabelle2007To: isabelle-users@cl.cam.ac.ukIsabelle2007 is finally available.This release introduces fundamental changes over Isabelle2005, see theNEWS file in the distribution for more details. Numerous existingconcepts have been generalized and re-implemented based on novelsystem architecture. New theories and proof tools have been added(mostly for HOL). Some highlights are:* Support for nominal datatypes (binding structures) due to theHOL-Nominal logic.* General local theory infrastructure for specifications depending onparameters 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.* Built-in Metis prover, external linkup for automated provers, and'sledgehammer' command for automated proof synthesis.* Auto quickcheck: toplevel goals are tested for counterexamplesautomatically when they are stated.* Second generation code generator for a subset of HOL, targeting SML,Haskell, and OCaml.* Command 'normal_form' and method "normalization" for evaluatingterms with free variables.* Full list comprehension syntax for HOL.* Much improved algebraic capabilities, including Groebner bases.* Embedding of ML code into theories with static references to thelogical context (via antiquotations).* Parallel loading of theories based on native multicore support inPoly/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/