Re: [isabelle] Destruction rules setup



On 14.07.2015 22:55, W. Douglas Maurer wrote:
> 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

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.