Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl id <12426-0@swan.cl.cam.ac.uk>; Fri, 8 Nov 1991 16:15:01 +0000 Received: by ted.cs.uidaho.edu (15.11/1.34) id AA21663; Fri, 8 Nov 91 08:05:07 pst Reply-To: info-hol@ted Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@ted.cs.uidaho.edu Received: from [128.232.0.56] by ted.cs.uidaho.edu (15.11/1.34) id AA21656; Fri, 8 Nov 91 08:04:58 pst Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl id <11980-0@swan.cl.cam.ac.uk>; Fri, 8 Nov 1991 16:04:53 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Re: witnesses In-Reply-To: Your message of Thu, 07 Nov 91 10:43:15 -0800. <9111071843.AA23035@cis.Stanford.EDU> Date: Fri, 08 Nov 91 16:04:48 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.985:08.10.91.16.04.58"@cl.cam.ac.uk> Futher to Paul's message, I should add that I shall shortly be working on an experimental extension to the HOL logic in which one can quantify over type variables. If the details work out smoothly, this should help to solve the problems Paul mentioned. But an implementation, I hasten say, is quite a long way off yet. Tom