Received: by 10.180.101.9 with SMTP id fc9mr674635wib.3.1351781744868;
        Thu, 01 Nov 2012 07:55:44 -0700 (PDT)
Path: q13ni123830wii.0!nntp.google.com!goblin3!goblin1!goblin.stu.neva.ru!uio.no!nntp.uio.no!.POSTED!not-for-mail
From: Tobias Nipkow <nip...@in.tum.de>
Newsgroups: fa.isabelle
Subject: Re: [isabelle] Type restrictions;
 document preparation [Re:  Started auction theory toolbox;
 announcement, next steps, and questions]
Date: Thu, 01 Nov 2012 14:55:44 UTC
Organization: Internet mailing list
Lines: 16
Sender: cl-isabelle-users-boun...@lists.cam.ac.uk
Message-ID: <fa.mjQ0a+dTwoo2vrCtyq3BsLFkOiU@ifi.uio.no>
References: <fa.g9J/+y5/aEMBIaGzLB/0eyYYB/k@ifi.uio.no> <fa.XHv+1mHdNtUGyNEAaMbRAheePp0@ifi.uio.no>
NNTP-Posting-Host: mail-jess.uio.no
Mime-Version: 1.0
X-Trace: readme.uio.no 1351781744 9983 129.240.7.9 (1 Nov 2012 14:55:44 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Thu, 1 Nov 2012 14:55:44 +0000 (UTC)
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
	rv:16.0) Gecko/20121026 Thunderbird/16.0.2
To: cl-isabelle-us...@lists.cam.ac.uk
X-Cam-AntiVirus: not scanned (internal relaying)
X-Cam-SpamDetails: not scanned
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
X-Cam-AntiVirus: no malware found
X-Cam-SpamDetails: score -2.3 from SpamAssassin-3.3.2-1404039 
	* -2.3 RCVD_IN_DNSWL_MED RBL: Sender listed at http://www.dnswl.org/,
	*      medium trust
	*      [131.159.0.8 listed in list.dnswl.dnsbl.ja.net]
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
X-Virus-Scanned: amavisd-new at informatik.tu-muenchen.de
In-Reply-To: <50926D50.6030101@cs.bham.ac.uk>
X-Enigmail-Version: 1.4.5
X-BeenThere: cl-isabelle-us...@lists.cam.ac.uk
X-Mailman-Version: 2.1.8
List-Id: Isabelle Users List <cl-isabelle-users.lists.cam.ac.uk>
List-Unsubscribe: <https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users>, 
	<mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=unsubscribe>
List-Archive: <https://lists.cam.ac.uk/pipermail/cl-isabelle-users>
List-Post: <mailto:cl-isabelle-us...@lists.cam.ac.uk>
List-Help: <mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=help>
List-Subscribe: <https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users>, 
	<mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=subscribe>
Original-Date: Thu, 01 Nov 2012 15:52:08 +0100
Original-Message-Id: <50928C98.5050...@in.tum.de>
Original-References: <5091D94E.90...@gmail.com> <50926D50.6030...@cs.bham.ac.uk>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

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