Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 7 Oct 1993 14:05:06 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA28153; Thu, 7 Oct 93 05:43:12 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from wasa.shh.fi by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA28149; Thu, 7 Oct 93 05:43:09 -0700 Received: from charon.wasa.shh.fi by wasa.shh.fi (4.1/291091(up)) id AA02455; Thu, 7 Oct 93 14:43:24 +0200 Received: From PAMIR/WORKQUEUE by charon.wasa.shh.fi via Charon-4.0A-VROOM with IPX id 100.931007144501.416; 07 Oct 93 14:45:12 +0500 Message-Id: To: info-hol@cs.uidaho.edu From: jwright@wasa.shh.fi Organization: Swedish School of Econ. Vasa Date: 7 Oct 1993 14:42:08 EET Subject: Announcing a contribution Priority: normal X-Mailer: Pegasus Mail/Mac v2.02 This is a message to announce a new contribution to HOL. I have been doing some work on Representing higher order logic proofs in HOL The results (including documentation in a dvi-file) are now available in the HOL contrib directory in Cambridge (i.e., hvg/contrib after you've anon-ftp'd to ftp.cl.cam.ac.uk). The complete contribution is in the subdirectory HOLproof and there is a compressed tarfile with the same contents in 00-Tarfiles. Any comments and/or questions are more than welcome. Joakim von Wright (jwright@wasa.shh.fi)