# HG changeset patch
# User wenzelm
# Date 1191266389 -7200
# Node ID 6bd8ec8f3fc85ad13680b26a61b709c667c20dc9
# Parent  f53f6b08e13a56c5dcf2c608571abffed0511d2a
preliminary material for Isabelle2007;

diff -r f53f6b08e13a -r 6bd8ec8f3fc8 ANNOUNCE
--- a/ANNOUNCE	Mon Oct 01 21:08:26 2007 +0200
+++ b/ANNOUNCE	Mon Oct 01 21:19:49 2007 +0200
@@ -1,30 +1,51 @@
-Subject: Announcing Isabelle2005
+Subject: Announcing Isabelle2007
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2005 is now available.
+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:
 
-This release provides substantial advances over Isabelle2004, see the
-first 1000 lines of NEWS in the distribution for more details.  Some
-highlights are:
+* New 'function' package for general recursive function definitions.
+
+* New version of 'inductive' package for inductive predicates;
+separate variant 'inductive_set'.
 
-* Interpretation of locale expressions in theories, locales, and proof
-contexts.
+* New basic specification elements 'definition', 'axiomatization',
+'abbreviation', 'notation'.
 
-* Substantial library improvements (HOL, HOL-Complex, HOLCF).
+* New 'class' package combination of axclass + locale interpretation.
 
-* Proof tools for transitivity reasoning.
+* Fully featured support for nominal datatypes (binding structures)
+due to the HOL-Nominal logic.
+
+* Various improvements in locale infrastructure (interpretation etc.)
 
-* General 'find_theorems' command (by term patterns, as
-intro/elim/simp rules 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.
 
-* Commands for generating ad-hoc draft documents.
+* General local theory infrastructure for specifications depending on
+parameters and assumptions (e.g. from locales, classes).
+
+* Second generation code-generator for a subset of HOL, targeting SML,
+Haskell, and OCaml.
 
-* Support for Unicode proof documents (UTF-8).
+* Improved support for arbitrary ML operations depending on the
+logical context.
 
-* Major internal reorganizations and performance improvements.
+* Parallel loading of theories based on native multicore support in
+Poly/ML 5.1.
 
 
-You may get Isabelle2005 from the following mirror sites:
+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/