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