Re: [isabelle] How to use Isabelle/Isar as a compiler?
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:
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).
On 04/05/2011 04:32 AM, Anh Le wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and