Re: [isabelle] Announcing Isabelle2013-2

On Mo, 2013-12-16 at 04:45 +0100, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius  
> <makarius at> a écrit:
> > Isabelle2013-2 is now available.
> >
> > […]
> Was probably already the same with prior version, still a quick comment on  
> document generation.
> When a proof contains a “sorry” and the proof is closed with an “oops”,  
> that's not really cheating, so may be building a document from a theory  
> containing not so real cheating, could terminate successfully without a  
> “Cheating requires quick_and_dirty mode!”.

I guess that this is technically nearly impossible, as "sorry" already
"proves" theorems in the kernel, that may escape the proof before you
abort it with oops.


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