Re: [isabelle] using Isabelle programmatically




On 04/09/2015 06:50 PM, Lars Noschinski wrote:
> context = ...
> T = Simplifier.rewrite context (Syntax.parse_term context "...")
> result =  Syntax.string_of_term context (the right hand side term of T)
> Lars has already written something about how to acquire a context.
> Depending on what you do with the terms in your program, it might be a
> good idea to use the YXML format to pass terms between Isabelle and your
> program. There have been some discussions on that subject in the past.
>
This is a good point. Thank you. We will use the simplified
expressions to generate some other Isabelle file, so for this
purpose we do not need the xml format.

Best regards,

Viorel





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