[isabelle] Intro, elim, dest modifiers



Hi,

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,
   Jason





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