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 <26979-0@swan.cl.cam.ac.uk>; Wed, 29 Apr 1992 07:46:31 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15425;
          Tue, 28 Apr 92 23:25:22 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA15417;
          Tue, 28 Apr 92 23:25:00 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <17303>;
          Wed, 29 Apr 92 08:24:44 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <10761>;
          Wed, 29 Apr 92 08:26:25 +0200
From: Tobias.Nipkow@De.TU-Muenchen.Informatik
To: info-hol@edu.uidaho.cs.ted
Cc: Larry.Paulson@uk.ac.cam.cl
In-Reply-To: Tom Melham's message of Tue, 28 Apr 92 23:09:27 +0200 <"swan.cl.ca.913:28.03.92.21.09.36"@cl.cam.ac.uk>
Subject: Well-founded recursion?
Message-Id: <92Apr29.082625met_dst.10761@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 29 Apr 92 08:26:23 +0200

The HOL instantiation of the generic theorem prover Isabelle provides
well-founded recursion. With a couple of days work you could port the defns
and thms to the real HOL system (or start using Isabelle :-)

Tobias