Email Gateway (Aug 19 2022 at 13:52): Email Gateway (Aug 19 2022 at 13:52):From: Gergely Buday <gbuday@gmail.com>
Hi,
prf and full_prf write out the proof object into the prepared LaTeX
document, as described in
4.2 Document Antiquotations
of the Isabelle reference manual. Is this functionality available from
Isabelle/ML? I would like to process the proof object.
Email Gateway (Aug 19 2022 at 13:53):From: Lars Noschinski <noschinl@in.tum.de>
Thm.proof_of returns you the proof of the theorem.
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
That is the "Isabelle/Isar reference manual", the former "Isabelle
reference manual" was just deleted in the last release.
To find how things are defined, you just use the normal C-hover click of
the Prover IDE. So if you spot something somewhere, you just make a
formally checked example like this:
text {* @{prf reflexive} *}
Then you ask the Prover IDE to jump to the source text for "prf". In the
target you continue with plain jEdit hypersearch etc. to get an idea how
it all fits together.
Since proof terms are rarely used, there might be some inconveniences and
snags on your way, but that is to be expected. For the current release,
I've made a few renovations together with Stefan Berghofer, but it is not
fully up-to-date in every sense.
Makarius
Last updated: Apr 29 2024 at 20:15 UTC