Email Gateway (Jan 31 2026 at 10:27): Email Gateway (Jan 31 2026 at 10:27):From: Gidon Ernst <gidon.ernst@lmu.de>
Dear all,
maybe someone can help:
How do I remove a rule from the intro! set?
I have tried:
declare <rule>[intro! del]
apply (auto intro! del: <rule>)
(and also with intro instead of intro!),
but both are invalid syntax.
The rule in question is predicate1I, which interferes with by intended
proof strategy.
Best,
--
Gidon Ernst
Software and Computational Systems Lab, LMU Munich
https://www.sosy-lab.org/people/ernst/
Email Gateway (Jan 31 2026 at 11:09):From: Makarius <makarius@sketis.net>
On 31/01/2026 11:27, Gidon Ernst wrote:
How do I remove a rule from the intro! set?
I have tried:declare <rule>[intro! del]
apply (auto intro! del: <rule>)(and also with intro instead of intro!),
but both are invalid syntax.
Use "rule del" here, either as attribute or method modifier.
Makarius
Last updated: Jan 31 2026 at 12:53 UTC