Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 19 Apr 1993 22:01:12 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13813; Mon, 19 Apr 93 09:11:12 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13808; Mon, 19 Apr 93 09:11:03 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Mon, 19 Apr 1993 17:10:27 +0100 To: info-hol@ted.cs.uidaho.edu Cc: Tom.Melham@cl.cam.ac.uk Subject: Book announcement -- Introduction to HOL. Date: Mon, 19 Apr 93 17:10:15 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.484:19.04.93.16.10.44"@cl.cam.ac.uk> Book on HOL now available ========================= Further to Mike Gordon's messages of 21 Feb 92 [archive 0454] and 23 Nov 92 [archive 0810], the following book is now available: Introduction to HOL: a theorem proving environment for higher order logic Edited by M. J. C. Gordon and T. F. Melham Cambridge University Press, 1993. 228 x 152 mm; 496 pp.; Full Canadian binding ISBN 0 521 44189 7 This is an edited version of a combination of the HOL tutorial and description, published in a format suitable for convenient reference at the terminal as well as regular reading. The term "Full Canadian" refers to a kind of spiral binding, a bit like that of the LaTeX manual but with covers that wrap round the spine (it looks quite good). The UK price of the book is 27.95 pounds sterling. I'm afraid I can't give a price in dollars at the moment. You can order from your bookseller, or you can contact CUP by email at the following addresses; they will be able to supply ordering details. TW10002@phx.cam.ac.uk [in the U.K. or Europe] mktg_cam@acfcluster.nyu.edu [in the U.S. or Canada] You can also contact CUP by post at: Customer Services Department Cambridge University Press The Edinburgh Building Cambridge, England, CB2 2RU. Note that any royalties from the book are going into a fund to support the HOL system and HOL-based activities. Tom