Email Gateway (Aug 18 2022 at 15:47): 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
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: Nov 21 2024 at 12:39 UTC