Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 4 Sep 1992 11:05:22 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01869; Fri, 4 Sep 92 02:50:14 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from [129.215.160.108] by ted.cs.uidaho.edu (16.6/1.34) id AA01864; Fri, 4 Sep 92 02:50:07 -0700 Received: from gilsay.dcs.ed.ac.uk by dcs.ed.ac.uk id aa20460; 4 Sep 92 10:45 BST To: Tom Melham Cc: info-hol@edu.uidaho.cs.ted, juan Subject: Re: Inductive Definitions Report. In-Reply-To: Your message of "Tue, 01 Sep 92 12:11:40 BST." <"swan.cl.ca.468:01.08.92.11.11.50"@cl.cam.ac.uk> Date: Fri, 04 Sep 92 10:45:05 +0100 From: Matt Fairtlough Message-Id: <9209041045.aa20460@dcs.ed.ac.uk> Dear Tom, I would like a copy of your technical report on inductively defined relations, please. I wonder if it would also be possible to get hold of a copy of Larry Paulson's old report on Well-founded recursion? I'm still very interested in your "dependent types" package for HOL (and in comparing it with the implementation of Martin-Lof type theory in ISABELLE-92). I'm leaving Edinburgh for a teaching post in Sheffield on 14/9/92, so I'd appreciate it if you could get the report(s?) to me by then. Thanks a lot, Matt.