Email Gateway (Aug 19 2022 at 09:04): Email Gateway (Aug 19 2022 at 09:04):From: Tobias Nipkow <nipkow@in.tum.de>
After a false start and some experiments I have now converged on (essentially)
Thomas' solution, but integrated into rewr_conv. It lets resolution do the work
and is thus immune against funny matchers. No point in doing anything cleverer.
No theory in the distribution or the AFP were affected and Peter's example works
fine now.
Enjoy
Tobias
Last updated: Nov 21 2024 at 12:39 UTC