[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