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.
You probably need to enable proofterms first. For HOL, try loading HOL-Proofs
instead of the standard HOL
image by starting Isabelle using isabelle jedit -l HOL-Proofs
Last updated: Jul 15 2022 at 23:21 UTC