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
Robin Green wrote:
A question about transforming Isabelle proofs into really elementary,
In , 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