Email Gateway (Mar 21 2026 at 09:45): Email Gateway (Mar 21 2026 at 09:45):From: Florian Haftmann <florian.haftmann@cit.tum.de>
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
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Apr 07 2026 at 09:05 UTC