Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 3 Jun 1994 03:36:24 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03097;
          Thu, 2 Jun 1994 20:20:25 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from hp9000.csc.cuhk.hk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA03093;
          Thu, 2 Jun 1994 20:20:20 -0600
Received: from iist.unu.edu ([192.203.232.5]) by hp9000.csc.cuhk.hk 
          with SMTP (1.37.109.9/16.2) id AA1634837660;
          Fri, 3 Jun 1994 10:19:08 +0800
Received: from sif.iist.unu.edu by iist.unu.edu (4.1/SMI-4.1) id AA17038;
          Fri, 3 Jun 94 10:21:20 HKT
Received: from localhost by sif.iist.unu.edu (4.1/SMI-4.1) id AA25384;
          Fri, 3 Jun 94 10:21:10 HKT
Message-Id: <9406030221.AA25384@sif.iist.unu.edu>
To: users@iist.unu.edu, info-hol@leopard.cs.byu.edu
Subject: Review of the HOL book
Date: Fri, 03 Jun 94 10:21:03 +0800
From: Wong Wai <ww@iist.unu.edu>

I found a short review of the HOL book in `The Computer
Journal' Vol. 37, No. 2. Below is the last sentence of the
review:

		For those involved in formal methods, HOL is
	probably the most outstanding proof tool available and
	this book will certainly greatly assist newcomers to
	get to grips with the HOL system.

Wai