updated for release;
authorwenzelm
Wed, 06 Jun 2018 11:49:16 +0200
changeset 68392 9b4f60bdad54
parent 68391 c558a2202f32
child 68393 b2510432c94d
updated for release; tuned;
ANNOUNCE
CONTRIBUTORS
COPYRIGHT
NEWS
--- a/ANNOUNCE	Wed Jun 06 11:41:54 2018 +0200
+++ b/ANNOUNCE	Wed Jun 06 11:49:16 2018 +0200
@@ -1,32 +1,15 @@
-Subject: Announcing Isabelle2017
+Subject: Announcing Isabelle2018
 To: isabelle-users@cl.cam.ac.uk
 
-Isabelle2017 is now available.
+Isabelle2018 is now available.
 
-This version introduces many changes over Isabelle2016-1: see the NEWS
+This version introduces many changes over Isabelle2017: see the NEWS
 file for further details. Some notable points:
 
-* Experimental support for Visual Studio Code as alternative PIDE front-end.
-
-* Improved Isabelle/jEdit Prover IDE: management of session sources
-independently of editor buffers, removal of unused theories, explicit
-indication of theory status, more careful auto-indentation.
-
-* Session-qualified theory imports.
-
-* Code generator improvements: support for statically embedded computations.
-
-* Numerous HOL library improvements.
-
-* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
-(ported from HOL-Light).
-
-* Improved Nunchaku model finder, now in main HOL.
-
-* SQL database support in Isabelle/Scala.
+* FIXME.
 
 
-You may get Isabelle2017 from the following mirror sites:
+You may get Isabelle2018 from the following mirror sites:
 
   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle
   Munich (Germany)     http://isabelle.in.tum.de
--- a/CONTRIBUTORS	Wed Jun 06 11:41:54 2018 +0200
+++ b/CONTRIBUTORS	Wed Jun 06 11:49:16 2018 +0200
@@ -3,11 +3,11 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2018
+-----------------------------
 
 * May 2018: Manuel Eberl
-  Landau symbols and asymptotic equivalence (moved from the AFP)
+  Landau symbols and asymptotic equivalence (moved from the AFP).
 
 * May 2018: Jose Divasón (Universidad de la Rioja),
   Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
@@ -22,9 +22,8 @@
   Code generation with lazy evaluation semantics.
 
 * March 2018: Florian Haftmann
-  Abstract bit operations push_bit, take_bit, drop_bit, alongside
-  with an algebraic foundation for bit strings and word types in
-  HOL-ex.
+  Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
+  algebraic foundation for bit strings and word types in HOL-ex.
 
 * March 2018: Viorel Preoteasa
   Generalisation of complete_distrib_lattice
@@ -36,7 +35,8 @@
   A new conditional parametricity prover.
 
 * October 2017: Alexander Maletzky
-  Derivation of axiom "iff" in HOL.thy from the other axioms.
+  Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
+
 
 Contributions to Isabelle2017
 -----------------------------
--- a/COPYRIGHT	Wed Jun 06 11:41:54 2018 +0200
+++ b/COPYRIGHT	Wed Jun 06 11:49:16 2018 +0200
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 1986-2017,
+Copyright (c) 1986-2018,
   University of Cambridge,
   Technische Universitaet Muenchen,
   and contributors.
--- a/NEWS	Wed Jun 06 11:41:54 2018 +0200
+++ b/NEWS	Wed Jun 06 11:49:16 2018 +0200
@@ -4,8 +4,8 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2018 (August 2018)
+---------------------------------
 
 *** General ***