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-Proofsinstead of the standard
HOLimage by starting Isabelle using
isabelle jedit -l HOL-Proofs
Last updated: Jul 15 2022 at 23:21 UTC