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