Re: [isabelle] Verify proof of a single theorem



On 05/06/18 23:47, Makarius wrote:
> 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?
>>
> 
> Can you give more context to the intended application?

Just as a conclusion of the public thread: it looks to me like another
application of the new Isabelle server (for "headless PIDE"). See also
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions

I have given many demos and talks mentioning it recently, but it would
be nice if prospective users could start experimenting with it on time
before the Isabelle2018 becomes final, to make sure that it really works
as expected.


	Makarius




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