Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] dump tree


view this post on Zulip Email Gateway (Aug 18 2022 at 15:47):

From: Joao Marcos <botocudo@gmail.com>
Dear ALL:

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.

Or maybe some other tools for visualizing Isabelle proofs in tree format?

Yours,
JM

view this post on Zulip Email Gateway (Aug 18 2022 at 15:47):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joao,

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
signature.asc


Last updated: Mar 28 2024 at 20:16 UTC