Towards Isabelle2025-1-RC3 and AFP release

[Tobias Nipkow]

On 28/11/2025 17:53, Makarius wrote:
> Thus the feature additions by Tobias shortly after RC2 are included by accident, 
> because they are already on isabelle-release: 58fc6856e31a concerning HOL- 
> Library.While, 65734c8badd5 concerning newly introduced HOL- 
> Library.Time_Functions. Obscure corners of HOL-Library are not main HOL, after all.

It is called HOL-Library.While_Combinator and is one of the widely used theories 
in HOL-Library. Less judgemental and more factual is shorter and better.

Tobias
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4856 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251128/928113cc/attachment.bin>