Re: [isabelle] typo in isar-ref?
Am 15/07/2012 09:52, schrieb Ramana Kumar:
> Finally, if anyone knows about the proof terms that can be recorded, I'd
> love to eventually know exactly how (or whether) they relate to which parts
> of Isabelle reasoning. Do they perhaps encode resolution and assumption
> applications? Anything else?
The proof terms encode the primitive inferences in the framework logic, i.e. ==,
==> and !!. For details see
This archive was generated by a fusion of
Pipermail (Mailman edition) and