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; Mon, 3 Jan 1994 20:38:49 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA20089;
          Mon, 3 Jan 1994 13:29:51 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.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 AA20085;
          Mon, 3 Jan 1994 13:29:48 -0700
Received: from ninet.research.att.com by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA04230;
          Mon, 3 Jan 1994 12:27:09 -0800
Received: by ninet.research.att.com; Mon Jan 3 15:25 EST 1994
Received: by hunny.research.att.com (/\==/\ Smail3.1.25.1 #25.11) 
          id <m0pGvqc-0004C5C@hunny.research.att.com>; Mon, 3 Jan 94 15:25 EST
Received: from tiree.att.com by nfs.research.att.com 
          with smtp (Smail3.1.28.1 #12) id m0pGvrH-0000nCC;
          Mon, 3 Jan 94 15:26 EST
Message-Id: <m0pGvrH-0000nCC@nfs.research.att.com>
Date: Mon, 3 Jan 94 15:26 EST
From: elsa@research.att.com (Elsa Gunter)
Received: by tiree.att.com (4.1/SMI-4.1) id AA00547; Mon, 3 Jan 94 15:24:37 EST
To: info-hol@cs.uidaho.edu, myra@saul.cis.upenn.edu
Subject: slightly revised mutrec library

Myra VanInwegen and myself have made a few
modifications/corrections/extensions to the contributed library
"mutrec".  I still intend to replace this library in the not too
terribly distant future with one capable of handling a limited class
of function space occurrences, but it seemed wisest to make this
revised version available for general use in the meantime.

* Where the revised mutrec library can be found:
Via anonymous ftp from 

	 research.att.com:dist/ml/hol90/contrib/mutrec.tar.Z

* What's new:
- mutrec can now handle occurrences of type variables in
  specifications
- There is a new functor

ConsThmsFunc(MutRecDef:MutRecDefSig):
  sig
    val mutual_constructors_distinct : thm
    val mutual_constructors_one_one : thm
    val mutual_cases : thm
  end

the theroems that the term constructors are one-to-one, distinct, and
the cases theorem.

WARNING: The functor ConsThmsFunc is only intended as a very crude
temporary solution.  It can only be applied once per specification
since it makes definitions along the way.  It is your responsibility
to capture and store the theorems that it returns  so that you will
have them to use in subsequent sessions.