Email Gateway (Aug 22 2022 at 11:41): Email Gateway (Aug 22 2022 at 11:41):From: "Roger H." <s57076@hotmail.com>
Hello,
how can i apply the following lemma only once?
lemma "a = a + 1" (the soundness of the lemma is here irrelevant)
I mean i only want to rewrite the "a" with "a+1" only once..cause by default it will rewrite forever and i dont want that.
Thank you!
Email Gateway (Aug 22 2022 at 11:41):From: Lars Hupel <hupel@in.tum.de>
Hi Roger,
I mean i only want to rewrite the "a" with "a+1" only once..cause by default it will rewrite forever and i dont want that.
try the 'subst' method:
apply (subst your_theorem)
See also this recent thread:
<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/12006>
Cheers
Lars
Last updated: Apr 24 2024 at 08:20 UTC