NEWS: More uniform and scalable declarations of intro/elim/dest rules

[Makarius]

On 21/07/2025 17:45, Makarius wrote:
> *** General ***
> 
> * Declarations of intro/elim/dest rules for Pure and the Classical
> Reasoner (e.g. HOL) are handled more uniformly and efficiently: the
> order of rule declarations is maintained accurately, regardless of
> intermediate [rule del] declarations. Furthermore, [dest] is now a
> proper declaration on its own account, instead of the former expansion
> [elim_format, elim]. Consequently, [rule del] no longer deletes the
> [elim_format] of the given rule, only the original rule. Very rare
> INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual
> situations.
> 
> This refers to Isabelle/372273ab6ebb and AFP/eae86974a665.

After a few days of accumulating Isabelle + AFP "flight telemetry data", I 
have inspected 
https://isatest.sketis.net/devel/build_status/AFP_macOS_(macOS_14_Sonoma_Apple_Silicon)/index.html 
closely, if anything good or bad is to be seen there.

Conclusion: this change has now overall measurable effect on Isabelle/AFP, 
despite significant lack of scalability.


I found other performance changes elsewhere, and will report them separately.


	Makarius