[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.