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

http://www21.in.tum.de/~nipkow/pubs/tphols00.html

Tobias





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