Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 22 Apr 1993 13:32:32 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23741;
          Thu, 22 Apr 93 05:14:15 -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 AA23736;
          Thu, 22 Apr 93 05:14:05 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 22 Apr 1993 13:02:57 +0100
To: blok@cs.utwente.nl (Rintcius Blok)
Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
In-Reply-To: Your message of Thu, 22 Apr 93 13:37:07 +0200. <9304221137.AA28029@apollo.cs.utwente.nl>
Date: Thu, 22 Apr 93 13:02:50 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:295340:930422120804"@cl.cam.ac.uk>

Regarding

> We are interested in extending the HOL system in order to provide
> _indexed product types_ (labeled record types) for use in modeling
> object-oriented databases.  

> Hopefully, you or someone in your group could give us some idea of
> how difficult it would be to extend the HOL system with these constructs,
> which is something that _we_ are contemplating. 

In HOL88, it would take a *lot* of messy kernal hacking.  
HOL90 would be easier.

However, for this kind of activity perhaps you should think of
a logical framework like ISABELLE.  These are specifically designed
for jobs like this.

Tom