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


Last updated: Jul 15 2022 at 23:21 UTC