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


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