Re: [isabelle] Announcing Isabelle2013-2

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!”.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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