Re: [isabelle] How to use Isabelle/Isar as a compiler?



Hi,

the corresponding command is

  isabelle usedir -b HOL Name-of-output-Heap

reading the name of the used theory from the file ROOT.ML. In your case this should contain:

  use_thys ["MyTheory"];

In the above command, HOL is the name of the underlying heap image und the last argument is the name which you choose for the resulting heap image.

For a detailed description see the isabelle system manual, i.e.,

  isabelle doc system

(starting on page 20 in the documentation for Isabelle2011).

cheers

chris

On 04/05/2011 04:32 AM, Anh Le wrote:
Hi everyone,
Is there any way that we can use Isabelle/Isar as a compiler?
For example, how do we run a command like:
$ ./isabelle MyTheory.thy
And then isabelle will do as the Proof General processes the whole buffer,
and will return the first found error if it exists.

Thank you







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