Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 1 Sep 1993 16:57:53 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA12781;
          Wed, 1 Sep 93 08:48:19 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA12777; Wed, 1 Sep 93 08:48:18 -0700
Received: by panther.cs.uidaho.edu id AA05814 (5.65c/IDA-1.4.4 
          for info-hol@dworshak.cs.uidaho.edu); Wed, 1 Sep 1993 08:49:21 -0700
Date: Wed, 1 Sep 1993 08:49:21 -0700
From: Chris Toshok <toshok@cs.uidaho.edu>
Message-Id: <199309011549.AA05814@panther.cs.uidaho.edu>
To: info-hol@dworshak.cs.uidaho.edu
Subject: Mutually recursive type definition pacakges

Hello all,

  For my work with HOL, I really need to use mutually recursive datatypes.
I have been working with HOL88 2.01, but moving to HOL90 would not be a
problem.  What I need is a package that loads cleanly with the versions of
HOL88 and HOL90 (hol90.6) that we have, and is supported in some capacity
(at least being able to complain about a bug and have it get fixed).  Speed
of the package is not paramount, as most of the time I leave things running
all night anyway.  Pointers to packages and FTP sites would be appreciated.
Thanks in advance for all that reply.

====================================================================
Chris Toshok                   |  "To tuple is human,
                               |   to curry, divine"
toshok@snake.cs.uidaho.edu     |       - anonymous functional
toshok@uidaho.edu              |         programmer 
====================================================================