Towards Isabelle2025-1-RC3 and AFP release

[Makarius]

On 28/11/2025 18:35, Tobias Nipkow wrote:
> 
> 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.

"Widely used" would actually have been a point for excluding it from the 
release. But things are as they are now.


	Makarius