[isabelle] export proof state to file



Dear list,

is it possible to export the entire current proof state (or how it is
actually called) to an external file?
I assume it is possible to insert some code like
ML {* exportProofState "/tmp/export.txt" *}
but I am not even convinced that ML code can be contained within a proof.

Cheers
Sven





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