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 <17216-0@swan.cl.cam.ac.uk>; Tue, 28 Apr 1992 22:23:34 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12261;
          Tue, 28 Apr 92 14:09:54 -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 AA12257;
          Tue, 28 Apr 92 14:09:44 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <16909-0@swan.cl.cam.ac.uk>;
          Tue, 28 Apr 1992 22:09:32 +0100
To: Sreeranga Rajan <sree@ca.ubc.cs>
Cc: info-hol <info-hol@edu.uidaho.cs.ted>, Tom.Melham@uk.ac.cam.cl
Subject: Re: Well-founded induction?
In-Reply-To: Your message of 28 Apr 92 03:27:00 -0700. <322*sree@cs.ubc.ca>
Date: Tue, 28 Apr 92 22:09:27 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.913:28.03.92.21.09.36"@cl.cam.ac.uk>

Regarding Sreeranga Rajan's recent query:

> I was wondering if there has been effort in HOL to admit 
> recursive definitions by Well-founded induction wherein I could 
> ... etc

I think Wim Ploegaerts at IMEC (ploegaer@imec.be) has done something
roughly along these lines.

Tom