Email Gateway (Aug 22 2022 at 10:53): Email Gateway (Aug 22 2022 at 10:53):From: "W. Douglas Maurer" <maurer@email.gwu.edu>
I'm afraid I must not have been making myself clear. To give an
analogy: The direct effect of putting [simp] into the definition of a
rule is that the Simplifier then includes that rule as one of its
simprules. What is the direct effect, in that sense, of putting
[dest] into the definition of a rule? (One might ask the same
question, of course, about [intro] or [elim].) Thanks! -WDMaurer
Email Gateway (Aug 22 2022 at 10:53):From: Lars Noschinski <noschinl@in.tum.de>
The "dest", "intro", and "elim" attributes declare the rules to be used
as destruction, introduction, or elimination rules by tools using the
classical reasoner (e.g., fastforce, auto, blast).
These attributes are documented in the isar-ref manual, see the index.
The classical reasoner as a whole is documented in section 9.4.
-- Lars
Last updated: Apr 20 2024 at 01:05 UTC