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 assumption.

elim is a generalisation of dest; it can add multiple assumptions and !!-variables.

The !-modifier gives the rule high priority and (like Prolog's cut) prevents backtracking when that rule is chosen.

Larry

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 MHonArc.