Re: [isabelle] Export of proofs from Isabelle in "fully-expanded" form

Replying to my own post -

My apologies. I read the paragraph I quoted too hastily and misunderstood it! Dr. Watson has informed me that the export of proof derivations _was_ supported in Isabelle 98 (not Isabelle 99 as I misread it) - and is covered in his thesis, from which that quotation was taken.

(Any further information not covered in that thesis would of course be appreciated.)


Robin Green wrote:
A question about transforming Isabelle proofs into really elementary, long-winded form:


In [2], I found a tantalising hint which suggests that this feature became available in Isabelle 99:

"The Isabelle 98 version is used in this thesis, although a later version (Isabelle99) has since been released. These recent versions of Isabelle support the construction and export of proof derivations, a feature that was not available in early versions of Isabelle."

However, I've been unable to ascertain, by browsing the documentation, where this export feature that Watson refers to, is. Is it there but undocumented, have I missed it, or have I misunderstood what it is? Or is it simply not there?

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