# [isabelle] See the proof of a theorem

Hi,

Is there any command to see / dump / pretty-print a (partial) proof in
Isabelle? What I mean is:

- Before one has done "qed", while one is proving a theorem, there is
(I presume) a partial proof somewhere in the internals of the
system; maybe in the shape of a \lambda-term with (typed) holes /
placeholders, or in the shape of a tree of what rule / tactic
brought what proof state to what proof state, or both.

Can I see that partial proof? (People that know Coq will recognise
the "Show Proof." and "Show Tree." commands of Coq.)

- After one has done the "qed", the same data as before, except that
there will be proof will be complete.

(Something like "Print theorem_name." in Coq.)

Thanks for the information,

--
Lionel



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.