ANNOUNCE
author wenzelm
Tue Jul 01 14:52:08 2014 +0200 (2014-07-01)
changeset 57452 ecad2a53755a
parent 54639 5adc68deb322
child 57504 5cf245c62c4c
permissions -rw-r--r--
misc updates for release;
     1 Subject: Announcing Isabelle2014
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2014 is now available.
     5 
     6 This version significantly improves upon Isabelle2013-2, see the NEWS
     7 file in the distribution for more details.  Some highlights are:
     8 
     9 * Improved Isabelle/jEdit Prover IDE: navigation, completion,
    10   spell-checking, Query panel, Simplifier Trace panel.
    11 
    12 * Support for auxiliary files within the Prover IDE.
    13 
    14 * Support for official Standard ML within the Prover IDE,
    15   independently of Isabelle theory and proof development.
    16 
    17 * HOL: BNF datatypes and codatatypes within theory Main, with numerous
    18   add-on tools.
    19 
    20 * HOL tool enhancements: Nitpick, Sledgehammer.
    21 
    22 * HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    23   HOL-Probability.
    24 
    25 * HOL: internal SAT solver "cdclite" with models and proof traces.
    26 
    27 * HOL: updated SMT module, with support for SMT-LIB 2 and recent
    28   versions of Z3, as well as CVC3, CVC4.
    29 
    30 * Updated and extended manuals: codegen, datatypes, implementation,
    31   isar-ref, jedit, system.
    32 
    33 * System integration: improved support of LateX on Windows platform.
    34 
    35 
    36 You may get Isabelle2013-2 from the following mirror sites:
    37 
    38   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    39   Munich (Germany)     http://isabelle.in.tum.de/
    40   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/