Re: [isabelle] few questions about Isabelle/jEdit
The batch mode is when Isabelle is not running in interactive mode.
Similarly, you check a theory when you build a heap image or build the
documentation for it. If ever there is an error in a theory, the whole
process will fail. Most people want to at least produce a PDF file for
their theories, so the theory is always checked this way.
To understand all of this, you may have a look at “The Isabelle System
Manual” which is the file `doc/system.pdf`.
Le Sun, 20 Apr 2014 16:04:56 +0200, noam neer
<noamneer at gmail.com> a écrit:
how do I run it as batch job on windows ?
On Sun, Apr 20, 2014 at 2:20 PM, Lawrence Paulson
<lp15 at cam.ac.uk> wrote:
Everything is processed in parallel under the assumption that everything
above has been processed okay. It is quite normal for processing to
the end of the file even though significant parts of proofs are
to execute. You need to check that there is no red anywhere in the
The definitive test is to run it as a batch job.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and