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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and