Re: [isabelle] export proof state to file



On Fri, 4 Dec 2015, Sven Schneider wrote:

is it possible to export the entire current proof state (or how it is actually called) to an external file?

It depends what you mean by "proof state". The goal statement as a term? A pretty-printed version of it? Or the true internal state (which is opaque and cannot easily be serialized)?

The canonical meta-question: What is the intended application?


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.

See the isar-ref manual about various ML commands. Looking around a bit more, you will also see that Isabelle sources don't use camel case.


	Makarius




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