Re: [isabelle] dump tree

Hi Joao,

> Is there a single Isabelle command that allows one to inspect the
> *complete* proof state at a given point?
>   --- By "complete" I mean all the steps done so far, with enough information
>   for one to build the full natural deduction *tree* for the
> corresponding proof.

given that proof terms are turned on (select image HOL-Proofs and switch
"full proofs" on in PG), you can inspect finished proofs using "prf" and

Whether this is helpful for you depends on the particular application
you want to perform with proof trees, so don't hesitate to ask further
questions or to give more background.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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