| 
82063
 | 
     1  | 
Subject: Announcing Isabelle2025
  | 
| 
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
  |