Re: [isabelle] Intro, elim, dest modifiers
See Chapter 5 of the tutorial. To summarize:
intro denotes backward chaining, reducing goals to some goals.
dest denotes forward chaining, deducing a new assumption from an
elim is a generalisation of dest; it can add multiple assumptions
The !-modifier gives the rule high priority and (like Prolog's cut)
prevents backtracking when that rule is chosen.
On 27 Mar 2008, at 13:42, Jason Kirschenbaum wrote:
I'm trying to understand how to modify the classical reasoner to
add new rules. I'm pretty sure that the [intro], [elim] and [dest]
modifiers for theorems govern how the theorem will be used by the
reasoner. I'm having a hard time finding specific documentation on
how these modifiers work (include the differences between intro, and
intro! ). If someone could point me to a document that would
explain this, I would really appreciated it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and