Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] rewr_conv


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC