Re: [isabelle] generating isabelle theory files from ML modules?



If you mean are there ML functions which help generate theory file text, e.g. by building a parse tree and then printing it, then I believe the answer is "no, not at the moment" but yes, such a tool is needed if you want to manipulate proof scripts programmatically. I have wanted to do this for Proof General for a long time, but it seems difficult to achieve with Isar's extensible language and parsing combinators.

 - David.


Tuvshintur Tserendorj wrote:
hi,

Does someone know there exists anytool for generating isabelle theory files from ML modules (functions)?

Is such a tool needed?

cheers,
Tuvshintur






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