author | wenzelm |
Sat, 15 Aug 2015 19:42:35 +0200 | |
changeset 60937 | 51425cbe8ce9 |
parent 60125 | 2944cc4f4f56 |
child 62016 | 740c70a21523 |
permissions | -rw-r--r-- |
60016 | 1 |
Subject: Announcing Isabelle2015 |
9928 | 2 |
To: isabelle-users@cl.cam.ac.uk |
3 |
||
60016 | 4 |
Isabelle2015 is now available. |
54034 | 5 |
|
60016 | 6 |
This version improves upon Isabelle2014 in many ways, see the NEWS file in |
60116 | 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 |
|
60125 | 11 |
asynchronous print commands (e.g. Sledgehammer provers). |
60116 | 12 |
|
13 |
* Support for 'private' and 'qualified' name space modifiers. |
|
14 |
||
15 |
* Structural composition of proof methods (meth1; meth2) in Isar. |
|
57452 | 16 |
|
60116 | 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 |
||
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset
|
27 |
* New Eisbach proof method language and "match" method. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset
|
28 |
|
60116 | 29 |
* Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer, |
30 |
system. |
|
54034 | 31 |
|
12983 | 32 |
|
60016 | 33 |
You may get Isabelle2015 from the following mirror sites: |
9928 | 34 |
|
27085 | 35 |
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
17696 | 36 |
Munich (Germany) http://isabelle.in.tum.de/ |
14616 | 37 |
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |