# HG changeset patch # User wenzelm # Date 1528278556 -7200 # Node ID 9b4f60bdad54e7186b482e560f801732b0935124 # Parent c558a2202f3243b709f72c9f76304b65627da1d1 updated for release; tuned; diff -r c558a2202f32 -r 9b4f60bdad54 ANNOUNCE --- 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 diff -r c558a2202f32 -r 9b4f60bdad54 CONTRIBUTORS --- 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 ----------------------------- diff -r c558a2202f32 -r 9b4f60bdad54 COPYRIGHT --- 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. diff -r c558a2202f32 -r 9b4f60bdad54 NEWS --- 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 ***