# HG changeset patch
# User wenzelm
# Date 1428782956 -7200
# Node ID 6e6cc8c012a2424e17fa5768066863e348dad712
# Parent  3aceecdabed61a29d959f6dbc6fe640fccace8cf
updated for release;

diff -r 3aceecdabed6 -r 6e6cc8c012a2 ANNOUNCE
--- a/ANNOUNCE	Sat Apr 11 21:44:38 2015 +0200
+++ b/ANNOUNCE	Sat Apr 11 22:09:16 2015 +0200
@@ -1,40 +1,15 @@
-Subject: Announcing Isabelle2014
+Subject: Announcing Isabelle2015
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2014 is now available.
-
-This version significantly improves upon Isabelle2013-2, see the NEWS
-file in the distribution for more details.  Some highlights are:
-
-* Improved Isabelle/jEdit Prover IDE: navigation, completion,
-  spell-checking, Query panel, Simplifier Trace panel.
-
-* Support for auxiliary files within the Prover IDE, notably
-  Isabelle/ML.
-
-* Support for official Standard ML within the Prover IDE,
-  independently of Isabelle theory and proof development.
+Isabelle2015 is now available.
 
-* HOL: BNF datatypes and codatatypes within theory Main, with numerous
-  add-on tools.
-
-* HOL tool enhancements: Nitpick, Sledgehammer.
-
-* HOL: internal SAT solver "cdclite" with models and proof traces.
+This version improves upon Isabelle2014 in many ways, see the NEWS file in
+the distribution for more details. Important points are:
 
-* HOL: updated SMT module, with support for SMT-LIB 2 and recent
-  versions of Z3, as well as CVC3, CVC4.
-
-* HOL: numerous library enhancements: main HOL, HOL-Word,
-  HOL-Multivariate_Analysis, HOL-Probability.
-
-* System integration: improved support of LaTeX on Windows platform.
-
-* Updated and extended manuals: codegen, datatypes, implementation,
-  isar-ref, jedit, system.
+* FIXME
 
 
-You may get Isabelle2014 from the following mirror sites:
+You may get Isabelle2015 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
   Munich (Germany)     http://isabelle.in.tum.de/