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 sketis.net> 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.