NEWS: Simplifier declarations

Florian Haftmann florian.haftmann at cit.tum.de
Sat Mar 21 10:35:52 CET 2026


Changeset 8bc1ef6d46ae concludes a series which aims to cleanup and 
modernize the signature of the simplifier.

See particularly file src/Pure/raw_simplifier.ML for an overview on the 
current state of affairs.

First, I applied the transition to selected examples in our visible 
universe, to get an idea how this will work out in practice; since this 
turned out easier than expected, I continued to cover all the Isabelle 
distro as well as the AFP.

While this shows that it is possible to migrate realistic applications 
with limited resources, for big applications outside there it might be 
easier in the first instance to use a transition layer, especially wrt. 
old-style infixes like addsimps etc.; see NEWS for further details.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 25429 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260321/db98ac50/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260321/db98ac50/attachment-0001.sig>


More information about the isabelle-dev mailing list