diff -r 6d34097215be -r ab6ff69fc1a6 ANNOUNCE --- a/ANNOUNCE Fri Jan 24 10:56:59 2025 +0100 +++ b/ANNOUNCE Fri Jan 24 11:17:32 2025 +0100 @@ -1,31 +1,41 @@ Subject: Announcing Isabelle2024 To: isabelle-users@cl.cam.ac.uk -Isabelle2024 is now available. +Isabelle2025 is now available. -This version introduces various changes over Isabelle2023: see the +This version introduces many changes over Isabelle2024: see the NEWS file for further details. Here are various details: -* More robust and scalable support for distributed build clusters. +* Inner syntax: markup for blocks and type information about constants. -* Official support for ARM64 on Linux (notably Docker on Apple Silicon). +* Inner syntax: more scalable pretty-printing, based on bytes (blobs). + +* Inner syntax: more efficient folding of term abbreviations. -* HOL: various improvements of theory libraries, notably in HOL-Analysis. +* Inner syntax: more robust "no_syntax" declarations via bundles. + +* HOL: various improvements of theory libraries. -* HOL: updates and improvements of Sledgehammer. +* HOL: updates and improvements of Sledgehammer and external provers. + +* HOL: various improvements to code generation. -* ML: antiquotations for try-catch-finally. +* Isabelle/jEdit: various improvements to Output, including Search. -* ML: physical interrupts are now distinguished from runtime system failures. +* Isabelle/VSCode: various improvements, concerning markup, completions etc. + +* Document preparation: more markup for term output. -* System: support for global registry in TOML format. +* ML: value-oriented pretty printing using explicit Pretty.output_ops. + +* System: Find_Facts full-text search engine, with web interface. -* System: support the Go development environment (all platforms). +* System: Build_Manager in Isabelle/Scala, as replacement for Jenkins. -* System: bundled MLton now includes both Linux and macOS (Intel). +* System: more scalable type isabelle.Bytes, allow messages of many GiB. -You may get Isabelle2024 from the following mirror sites: +You may get Isabelle2025 from the following mirror sites: Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) https://isabelle.in.tum.de