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; Thu, 7 Jul 1994 14:49:16 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02738;
          Thu, 7 Jul 1994 07:38:09 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02734;
          Thu, 7 Jul 1994 07:38:05 -0600
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA03806;
          Thu, 7 Jul 1994 06:34:55 -0700
Received: from cormorant.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 7 Jul 1994 14:33:55 +0100
Received: by cormorant.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA23495;
          Thu, 7 Jul 94 14:33:49 BST
Date: Thu, 7 Jul 94 14:33:49 BST
From: Mike.Gordon@cl.cam.ac.uk
Message-Id: <9407071333.AA23495@cormorant.cl.cam.ac.uk>
To: heckman@cs.ucdavis.edu
Cc: info-hol@cs.uidaho.edu
In-Reply-To: <9407070421.AA27983@shangrila.cs.ucdavis.edu> (heckman@cs.ucdavis.edu)
Subject: Re: mappings


Jim Grundy says:

>Note that because VDM mappings are the same as Z functions, and because people
>have investigated Z in HOL you can be assured that what you want has been
>done before.  Check out the reference below, for a description of Mike's
>representation of Z in HOL (check out ICL Proof Power for another).

Further to this, take a look at contrib/Z on hol88.2.02 which contains
the paper Jim mentions and the supporting code (which is in a very
half-baked state).

Mike