Return-Path: 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, 28 Jan 1994 11:22:23 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26662; Fri, 28 Jan 1994 04:11:04 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26658; Fri, 28 Jan 1994 04:10:57 -0700 Received: from cormorant.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 28 Jan 1994 10:58:12 +0000 Received: by cormorant.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA29180; Fri, 28 Jan 94 10:58:08 GMT Date: Fri, 28 Jan 94 10:58:08 GMT From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9401281058.AA29180@cormorant.cl.cam.ac.uk> To: info-hol@leopard.cs.byu.edu Cc: Jonathan.Bowen@comlab.ox.ac.uk Subject: Z in HOL An experimental prototype shallow embedding of (part of) the Z specification notation in HOL88 is available by anonymous ftp: Site: ftp.cl.cam.ac.uk [128.232.0.56] Directory: hvg/contrib/Z File: READ-ME This requires HOL88 Version 2.02 (though a patch for AKCL Version 2.01 will load automatically). The prototype is liable to change, possibly drastically. It is based on joint work with Jonathan Bowen of Oxford. Mike Gordon P.S Serious users of Z are reminded that an industrial strength embedding of Z in HOL is available from ICL (ProofPower-server@win.icl.co.uk).