Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <15539-0@swan.cl.cam.ac.uk>; Fri, 21 Feb 1992 17:08:48 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA21775; Fri, 21 Feb 92 08:23:13 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from Sunset.AI.SRI.COM by ted.cs.uidaho.edu (16.6/1.34) id AA21771; Fri, 21 Feb 92 08:23:09 -0800 Received: from cam.sri.com by Sunset.AI.SRI.COM (4.1/SMI-4.1) id AA04962 for info-hol@ted.cs.uidaho.edu; Fri, 21 Feb 92 08:26:18 PST Received: from chepstow.cam.sri.com by cam.sri.com (4.1/4.16) id AA16958 for info-hol@ted.cs.uidaho.edu; Fri, 21 Feb 92 16:25:35 GMT Received: by chepstow.cam.sri.com (4.1/4.16) id AA25755 for info-hol@ted.cs.uidaho.edu; Fri, 21 Feb 92 16:25:34 GMT Date: Fri, 21 Feb 92 16:25:34 GMT From: Mike Gordon Message-Id: <9202211625.AA25755@chepstow.cam.sri.com> To: info-hol@edu.uidaho.cs.ted Subject: HOL book We are looking into having a combination of the HOL tutorial and description published as a conventional book by a commercial publisher. The LaTeX sources would still be distributed free. The purpose of the book would be to provide a nice version that was relatively cheap and easy to get. The expected cost would be under 50 dollars. Any profits would go into a fund to support HOL. If you think you might buy the book please let me know how many copies you might want. This is just to get an idea of the market inside the HOL community. I will add up the numbers and pass the total to the potential publisher. Responding now does not mean you will be expected to buy the book if and when it is produced -- the publisher just wants to get a feel for what the demand might be, i.e. whether it is worth their while producing a book. Mike Gordon