Re: [isabelle] Verify proof of a single theorem



On 05/06/18 22:25, Diego Marmsoler wrote:
> 
> I have a question regarding the use of Isabelle in batch mode: Is there a way to invoke Isabelle in a way to check the proof of a single theorem in a given theory file?
> 
> So, assuming i have a theory containing proofs for several theorems and i want Isabelle to check the proof of one theorem only.

Normally the purpose of batch mode is the check everything thoroughly.

It is possible to suppress whole theories via the "condition" option in
the session ROOT entry (see also the "system" manual, chapter 2.

It is also possible to use skip_proofs, although its meaning is not
clearly defined.


Can you give more context to the intended application?


	Makarius




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