Stream: Beginner Questions

Topic: ✔ How to print proof terms

view this post on Zulip waynee95 (Jan 26 2022 at 17:49):

Neither using prf nor following https://isabelle.in.tum.de/library/HOL/HOL-Proofs-ex/Proof_Terms.html
prints the proof term to the output, it only prints a question mark.

view this post on Zulip Simon Roßkopf (Jan 26 2022 at 18:10):

You probably need to enable proofterms first. For HOL, try loading HOL-Proofsinstead of the standard HOLimage by starting Isabelle using isabelle jedit -l HOL-Proofs

view this post on Zulip Notification Bot (Jan 26 2022 at 19:35):

waynee95 has marked this topic as resolved.

Last updated: Apr 25 2024 at 12:23 UTC