| author | wenzelm | 
| Tue, 29 Dec 2015 22:03:02 +0100 | |
| changeset 61966 | e90c42077767 | 
| 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: 
60116diff
changeset | 27 | * New Eisbach proof method language and "match" method. | 
| 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
 wenzelm parents: 
60116diff
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/ |