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
"thm_deps".

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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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