[isabelle] See the proof of a theorem
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and