*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 23 Nov 2012 14:39:30 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50AF54BF.1000606@cs.bham.ac.uk>*References*: <50916DB3.4030707@cs.bham.ac.uk> <B342CF2B-EEC3-4932-A98D-193702F57A14@cam.ac.uk> <5091CE53.6020006@cs.bham.ac.uk> <C76381F2-5127-48DF-B198-DE2B3AABEAB1@cam.ac.uk> <50AE3314.8060002@cs.bham.ac.uk> <50AE374C.9070402@in.tum.de> <50AE4F92.6080702@cs.bham.ac.uk> <50AF1DD3.5090702@in.tum.de> <50AF54BF.1000606@cs.bham.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

Am 23/11/2012 11:49, schrieb Christoph LANGE: > 2012-11-23 06:55 Tobias Nipkow: >> Am 22/11/2012 17:15, schrieb Christoph LANGE: >>> BTW, about "Programming and Proving": I had noticed this manual when I got >>> started with Isabelle, but then didn't take a closer look, as I was misled by >>> the "Programming". I thought it was some specific guide on verifying functional >>> programs. >> >> In a way it is. It starts from a functional programming perspective. If you have >> a suggestion for a better title, let me know. > > OK, got the point. Now I really can't imagine a better title. > > But I could imagine a better _guidance_, both on the documentation website > (http://isabelle.in.tum.de/documentation.html) and in the "doc/Contents" file of > the Isabelle installation (at least I have > /usr/share/doc/isabelle-2012/doc/Contents when installing from the Gentoo Linux > package). > > On the website, Prog&Prove is listed first, but under a section header > "Miscellaneous tutorials". The section title could be changed to "Getting > started", and each document link could be followed by a few words of > explanation, e.g.: > > Programming and Proving in Isabelle/HOL – Isabelle by example; read this first I think most of the titles are self-explanatory, and indicate that they are special manuals. Except for the first two. But all of them come with an abstract or intro, and prog-prove explains quite clearly what it is about (and mentions that the second one is old fashioned). You might want to also have this abstract on the web page, but that would require yet more mechanisms. However, there is a small linguistic point, which you may or may not have intended to make: "Miscellaneous" material usually comes at the end. These are "Tutorials", no qualification. The next subsection isn't called "Miscellaneous Reference Manuals" either, and the whole section is called "Tutorials and manuals". Makarius, could you drop the "Miscellaneous", please? Tobias > Similarly, the doc/Contents file should not merely restate the _titles_ of the > documents, but provide the same extra information. > > Cheers, > > Christoph >

**Follow-Ups**:

**References**:**[isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Lawrence Paulson

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Tobias Nipkow

**Re: [isabelle] ?spam? Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] ?spam? Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Tobias Nipkow

**[isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]***From:*Christoph LANGE

- Previous by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Previous by Thread: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Next by Thread: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list