Stream: Beginner Questions

Topic: How do I show a proof tree for an existing proof?

Ant S. (Feb 14 2026 at 16:41):

I have been playing around with prf and full_prf. Suppose I have some proof term that has been proven:

lemma simp1 [simp] : "app xs Nil = xs"
  apply (induct xs)
  apply (auto)
  done

If I do prf simp1 or full_prf simp1, I get ? ∙ (Pure.PClass type_class ⋅ TYPE(?'a)), which I don't know how to read. While this usually not something people apparently look for in Isabelle, I want something akin to Rocq's Show Proof. I tried switching my environment to HOL-Proofs, to no avail, following this SO thread as reference: https://stackoverflow.com/questions/30688177/how-to-see-step-by-step-reasoning-of-isabelle-proofs.

Again, I do understand why this is usually not of interest, but I would find it quite helpful.

Ant S. (Feb 14 2026 at 20:12):

Nevermind, it was full_prf, I just received no indication that HOL-Proofs needed to be compiled

Ant S. (Feb 14 2026 at 20:13):

there's no option to mark this as resolved, so if an admin could do that or give people permission to, that'd be fantastic

Last updated: Mar 04 2026 at 20:34 UTC