Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <18331-0@swan.cl.cam.ac.uk>; Tue, 9 Jun 1992 19:48:49 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26319;
          Tue, 9 Jun 92 11:23:14 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26315;
          Tue, 9 Jun 92 11:22:54 -0700
Received: from teal.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <17941-0@swan.cl.cam.ac.uk>; Tue, 9 Jun 1992 19:23:08 +0100
To: symdchon@au.edu.anu.mehta (donald syme )
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl, kevin@uk.ac.ed.dcs
Subject: Re: HOL: Struggling with mutually recursive types
In-Reply-To: Your message of Tue, 09 Jun 92 13:24:02 -0500. <9206090324.AA03336@mehta>
Date: Tue, 09 Jun 92 19:23:04 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.954:09.05.92.18.23.25"@cl.cam.ac.uk>

Re Donald Syme's recent message:

> I am a fairly new HOL user, and am presently working on entering the
> formal definition of ML into HOL.  Most of the work has already been
> done, but some of the problems with mutually recursive types were never
> solved by the guy whose work I'm taking over. ... etc

Regarding mutually recursive type definitions, Kevin Mitchell at
Edinburgh (kevin@uk.ac.ed.dcs) has a student who seems to have done a
good job at implementing these in general.  I have encouraged him to get
the implementation in shape for the HOL library.

By the way, "entering the formal definition of ML into HOL" seems to be
quite a popular project these days.  I'm aware of at least two other
groups working (or proposing to work) on this.  I leave it to them to
announce themselves on info-hol, if they wish.

Tom