80080
|
1 |
Subject: Announcing Isabelle2024
|
9928
|
2 |
To: isabelle-users@cl.cam.ac.uk
|
|
3 |
|
81967
|
4 |
Isabelle2025 is now available.
|
60116
|
5 |
|
81967
|
6 |
This version introduces many changes over Isabelle2024: see the
|
76108
|
7 |
NEWS file for further details. Here are various details:
|
73010
|
8 |
|
81967
|
9 |
* Inner syntax: markup for blocks and type information about constants.
|
78296
|
10 |
|
81967
|
11 |
* Inner syntax: more scalable pretty-printing, based on bytes (blobs).
|
|
12 |
|
|
13 |
* Inner syntax: more efficient folding of term abbreviations.
|
71485
|
14 |
|
81967
|
15 |
* Inner syntax: more robust "no_syntax" declarations via bundles.
|
|
16 |
|
|
17 |
* HOL: various improvements of theory libraries.
|
68545
|
18 |
|
81967
|
19 |
* HOL: updates and improvements of Sledgehammer and external provers.
|
|
20 |
|
|
21 |
* HOL: various improvements to code generation.
|
74651
|
22 |
|
81967
|
23 |
* Isabelle/jEdit: various improvements to Output, including Search.
|
78493
|
24 |
|
81967
|
25 |
* Isabelle/VSCode: various improvements, concerning markup, completions etc.
|
|
26 |
|
|
27 |
* Document preparation: more markup for term output.
|
71485
|
28 |
|
81967
|
29 |
* ML: value-oriented pretty printing using explicit Pretty.output_ops.
|
|
30 |
|
|
31 |
* System: Find_Facts full-text search engine, with web interface.
|
68545
|
32 |
|
81967
|
33 |
* System: Build_Manager in Isabelle/Scala, as replacement for Jenkins.
|
78455
|
34 |
|
81967
|
35 |
* System: more scalable type isabelle.Bytes, allow messages of many GiB.
|
76155
|
36 |
|
12983
|
37 |
|
81967
|
38 |
You may get Isabelle2025 from the following mirror sites:
|
9928
|
39 |
|
68599
|
40 |
Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
|
|
41 |
Munich (Germany) https://isabelle.in.tum.de
|
80080
|
42 |
Sydney (Australia) https://proofcraft.systems/isabelle/index.html
|
68599
|
43 |
Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle
|