ANNOUNCE
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 60125 2944cc4f4f56
child 62016 740c70a21523
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 Subject: Announcing Isabelle2015
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2015 is now available.
     5 
     6 This version improves upon Isabelle2014 in many ways, see the NEWS file in
     7 the distribution for more details. Some important points are as follows.
     8 
     9 * Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
    10 support for BibTeX files, improved graphview panel, improved scheduling for
    11 asynchronous print commands (e.g. Sledgehammer provers).
    12 
    13 * Support for 'private' and 'qualified' name space modifiers.
    14 
    15 * Structural composition of proof methods (meth1; meth2) in Isar.
    16 
    17 * HOL: BNF datatypes and codatatypes are now standard.
    18 
    19 * HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
    20 new free (!) version of Z3.
    21 
    22 * HOL: numerous library refinements and enhancements.
    23 
    24 * New proof method "rewrite" for single-step rewriting with subterm
    25 selection based on patterns.
    26 
    27 * New Eisbach proof method language and "match" method.
    28 
    29 * Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
    30 system.
    31 
    32 
    33 You may get Isabelle2015 from the following mirror sites:
    34 
    35   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    36   Munich (Germany)     http://isabelle.in.tum.de/
    37   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/