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 <13979-0@swan.cl.cam.ac.uk>; Wed, 22 Apr 1992 17:49:44 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25384;
          Wed, 22 Apr 92 09:38:36 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA25379; Wed, 22 Apr 92 09:38:31 -0700
Received: from localhost by panther.cs.uidaho.edu with SMTP 
          id AA13082 (5.65c/IDA-1.4.4 for info-hol@ted);
          Wed, 22 Apr 1992 09:42:49 -0700
Message-Id: <199204221642.AA13082@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: mutual recursion
Date: Wed, 22 Apr 92 09:42:49 -0700
From: Phil Windley <windley@edu.uidaho.cs.panther>
X-Mts: smtp


Hi,

Has anyone modified the mutual recursion stuff in the contrib directory to
work with HOL 2.0?  I tried loading and some of the proof scripts no longer
work.  Before I do it myslef, I wanted to be sure that I wasn't duplicating
effort.  

--phil--