Re: [isabelle] Turnstile



On 07/06/16 08:53, Peter Lammich wrote:
> 
> By the very design of Isabelle, every theorem has been proved (or has a
> pending future proof attached [Makarius, correct me if I'm wrong
> here ;)])

A thm value is indeed only a promise to finish a proof eventually. For
fully authentic results, one needs to do a batch run with "isabelle
build", which forms a global join on all open ends in the very end, and
potential errors are exposed.

This reform of thm-ness goes back to 2007/2008, when parallel proof
construction in Isabelle emerged for the first time.


	Makarius






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