ANNOUNCE
author wenzelm
Wed Jan 06 16:17:50 2016 +0100 (2016-01-06)
changeset 62084 969119292e25
parent 62064 d9874039786e
child 62190 ec5703538300
permissions -rw-r--r--
misc tuning for release;
     1 Subject: Announcing Isabelle2016
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2016 is now available.
     5 
     6 This version improves upon Isabelle2015 in many ways, see the NEWS file in the
     7 distribution for further details. Some highlights are as follows:
     8 
     9 * Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel
    10 and more asynchronous task management within the prover/GUI.
    11 
    12 * Additional Isar language elements for structured statements and proofs.
    13 
    14 * Document language refinements, with Markdown-like text structure.
    15 
    16 * More Isabelle symbols in theory and document sources.
    17 
    18 * Pure/HOL: uniform treatment of overloaded constant definitions versus type
    19 definitions; upgrade of HOL typedef to definitional principle.
    20 
    21 * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
    22 
    23 * HOL library additions and improvements, notably HOL-Multivariate_Analysis,
    24 HOL-Probability, HOL-Data_Structures.
    25 
    26 * Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
    27 ML), per-thread profiling, native Windows version (32bit and 64bit).
    28 
    29 
    30 You may get Isabelle2016 from the following mirror sites:
    31 
    32   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    33   Munich (Germany)     http://isabelle.in.tum.de/
    34   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/