Re: [isabelle] using Isabelle programmatically



> How can this be done programmatically? Should I use
> "isabelle_process" or "isabelle console"?

First of all, there's 'Simplifier.rewrite':

MLâSimplifier.rewrite @{context} @{cterm "rev []"}â

... which results in

val it = "rev [] â []": thm

This should be an easy-enough interface to perform just what you need.


Second, there's the question how to invoke just this bit. I think
'isabelle console' is out â quoting from the system manual:

"Interaction works via the raw ML toplevel loop: this is neither
Isabelle/Isar nor Isabelle/ML within the usual formal context. Some
useful ML commands at this stage are cd, pwd, use, use_thy, use_thys."

'isabelle_process' is even more low-level.

In which environment do you intend to invoke the simplifier? In some
program of yours? Via bash? Something else? Repeatedly, or just one-off?


Cheers
Lars

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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