| author | nipkow | 
| Thu, 12 Nov 2015 11:22:26 +0100 | |
| changeset 61644 | b1c24adc1581 | 
| 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/  |