[isabelle] Intro, elim, dest modifiers


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.

Thanks in advance,

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