preliminary material for Isabelle2007;
Mon, 01 Oct 2007 21:19:49 +0200
changeset 24802 6bd8ec8f3fc8
parent 24801 f53f6b08e13a
child 24803 38577b4b1fde
preliminary material for Isabelle2007;
--- 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
-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
+* 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
+* 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)
   Munich (Germany)