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
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