prepared for Isabelle2008;
Wed, 28 May 2008 22:50:30 +0200
changeset 27005 739d239ba514
parent 27004 616c553c7cf1
child 27006 6ca0c942a25c
prepared for Isabelle2008;
--- a/ANNOUNCE	Wed May 28 22:13:31 2008 +0200
+++ b/ANNOUNCE	Wed May 28 22:50:30 2008 +0200
@@ -1,54 +1,15 @@
-Subject: Announcing Isabelle2007
+Subject: Announcing Isabelle2008
-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).  Some highlights are:
-* 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.
+Isabelle2008 is now available.
-* 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 counterexamples
-automatically when they are stated.
-* Second generation code generator for a subset of HOL, targeting SML,
-Haskell, and OCaml.
+This release mostly consolidates Isabelle2007, see the NEWS file in
+the distribution for more details.  Some notable improvements are:
-* Command 'normal_form' and method "normalization" for evaluating
-terms 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 the
-logical context (via antiquotations).
-* Parallel loading of theories based on native multicore support in
-Poly/ML 5.1.
+* ...
-You may get Isabelle2007 from the following mirror sites:
+You may get Isabelle2008 from the following mirror sites:
   Cambridge (UK)
   Munich (Germany)