# HG changeset patch
# User wenzelm
# Date 1451662847 -3600
# Node ID 2ecee4679f9936f8aaaf4abd624e2591d884aec8
# Parent  b270f2b9bef8b2917549482e3874e4a180b31b66
updated for release;

diff -r b270f2b9bef8 -r 2ecee4679f99 ANNOUNCE
--- a/ANNOUNCE	Fri Jan 01 16:39:10 2016 +0100
+++ b/ANNOUNCE	Fri Jan 01 16:40:47 2016 +0100
@@ -3,11 +3,28 @@
 
 Isabelle2016 is now available.
 
-This version improves upon Isabelle2015 in numerous ways, see the NEWS
-file in the distribution for further details. Some highlights are as
-follows.
+This version improves upon Isabelle2015 in many ways, see the NEWS file in the
+distribution for further details. Some highlights are as follows:
+
+* Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel
+and more asynchronous task management within the prover/GUI.
+
+* Additional Isar language elements for structured statements and proofs.
+
+* Document language refinements, with Markdown-like text structure.
 
-* FIXME
+* More Isabelle symbols in theory and document sources.
+
+* Pure/HOL: uniform treatment of overloaded constant definitions versus type
+definitions; upgrade of HOL typedef to definitional principle.
+
+* HOL tool enhancements: quickcheck, sledgehammer, nitpick, transfer.
+
+* Many HOL library improvements, including advanced topological concepts and
+integration theory ported from HOL Light.
+
+* Upgrade to Poly/ML 5.6 with debugger IDE for Isabelle/ML and Standard ML,
+per-thread profiling, native support for Windows (32bit and 64bit).
 
 
 You may get Isabelle2016 from the following mirror sites: