Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 19 May 1993 14:28:01 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28461; Wed, 19 May 93 06:10:40 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28456; Wed, 19 May 93 06:10:34 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 19 May 1993 14:08:17 +0100 To: schneide Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: First-Order Reasoning and HOL In-Reply-To: Your message of "Wed, 19 May 93 14:38:48 +0700." <9305191239.AA28435@ted.cs.uidaho.edu> Date: Wed, 19 May 93 14:08:08 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:115350:930519130826"@cl.cam.ac.uk> > Is there a chance, that HOL can be extended to compare with those systems? Well, for a start someone could program up Isabelle's fast_tac (and related tactics) in HOL. As far as I can tell, this should be fairly straightforward. The Isabelle documentation seems to offer a sufficiently detailed description to reproduce the effect in HOL (hey... science!). This would make a good student project. Any volunteers? > Nuprl and Veritas both have dependent types, but HOL has nothing of the > mentioned tactics. See my paper with Bart Jacobs on faking dependent types in HOL. It's in ftp.cl.cam.ac.uk in hvg/papers. Tom PS: for fast_tac see the info-hol archive, Harrison-numbers 0670 and 1228.