Return-Path: Delivery-Date: Received: from lal.cs.byu.edu (actually leopard.cs.byu.edu !OR! info-hol-request@lal.cs.byu.edu) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 16 Sep 1994 11:47:30 +0100 Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA28781; Fri, 16 Sep 1994 04:40:55 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by lal.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA28773; Fri, 16 Sep 1994 04:40:47 -0600 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 16 Sep 1994 10:00:19 +0100 To: theorem-provers@mc.lcs.mit.edu, info-hol@lal.cs.byu.edu, logic@cs.cornell.edu, bra-types@cs.chalmers.se, isabelle-users@cl.cam.ac.uk Subject: ISABELLE BOOK NOW AVAILABLE Date: Fri, 16 Sep 94 10:00:12 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:063980:940916090111"@cl.cam.ac.uk> Isabelle: A Generic Theorem Prover by Lawrence C. Paulson, with contributions by Tobias Nipkow Springer Lecture Notes in Computer Science 828 Price: DM 66.00 XVII+321 pages, 1994. This book provides complete documentation of the theorem prover Isabelle. It includes an introduction, a general reference section, and documentation of the main logics provided with Isabelle. The book is closely based on the three Isabelle manuals distributed electronically with Isabelle. But it is a single volume with a global index. Mosaic users can call up a description of Isabelle via the URL http://www.cl.cam.ac.uk/Research/HVG/isabelle.html A plain text version is available by ftp from ftp.cl.cam.ac.uk, file ml/isabelle.txt. An errata list for the book is available using Mosaic or ftp: ftp://ftp.cl.cam.ac.uk/ml/ERRATA.txt Lawrence C. Paulson Computer Laboratory University of Cambridge Cambridge CB2 3QG England