Re: [isabelle] Type restrictions; document preparation [Re: Started auction theory toolbox; announcement, next steps, and questions]



Am 01/11/2012 13:38, schrieb Christoph LANGE:
> Plus, a question to everyone reading this: I haven't worked with the Tutorial
> too much, but mainly consulted the Isar Reference.  The Tutorial does proofs in
> the "apply(rule)" style, which we don't consider helpful for our target
> audience; we prefer textbook style.  Of course, I'm sure, for "apply(rule)"
> proof there is a straightforward translation to Isar, but for me, being a
> relative beginner, this is not yet _so_ straightforward.

If you look at the documentation page
http://isabelle.in.tum.de/documentation.html you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply".

Tobias





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