Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rewriting with Equivalence Relations in Isabel...

view this post on Zulip Email Gateway (Aug 19 2022 at 17:23):

From: Andrew Gacek <andrew.gacek@gmail.com>
Is there a way to get the Isabelle rewriting to use an alternate
equivalence relation rather than just equality? I've seen this before in
ACL2 [1], but I couldn't find anything similar for Isabelle/HOL.

Thanks,
Andrew

[1] http://link.springer.com/article/10.1007/s10817-007-9095-9

view this post on Zulip Email Gateway (Aug 19 2022 at 17:23):

From: Tobias Nipkow <nipkow@in.tum.de>
Unfortunately the answer is No. It could be done but requires some work...

Tobias
smime.p7s

Last updated: Apr 25 2024 at 04:18 UTC