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:

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

Is such a tool needed?


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