Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET
          with NIFTP to fgate (PP) id <3484-0@swan.cl.cam.ac.uk>;
          Tue, 4 Jun 1991 20:24:00 +0100
Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk
          with SMTP inbound id <21787-0@sun2.nsfnet-relay.ac.uk>;
          Tue, 4 Jun 1991 20:20:19 +0100
Received: from iris.ucdavis.edu by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP
          id aa14363; 4 Jun 91 19:31 BST
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA17447;
          Tue, 4 Jun 91 11:55:41 -0700
Received: from computer-lab.cambridge.ac.uk by sun2.nsfnet-relay.ac.uk
          via JANET with NIFTP id <19656-0@sun2.nsfnet-relay.ac.uk>;
          Tue, 4 Jun 1991 18:07:39 +0100
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP)
          id <1761-0@swan.cl.cam.ac.uk>; Tue, 4 Jun 1991 18:10:13 +0100
To: info-hol@edu.ucdavis.iris.cs.ucdavis.edu
Subject: survey of applications
Date: Tue, 04 Jun 91 18:10:10 +0100
From: Sara.Kalvala@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.764:04.05.91.17.10.15"@cl.cam.ac.uk>



Hello,

The list of projects using HOL I've put together a few months back
seems to have been surprisingly popular - many people have asked for
it and it's been distributed at a course on HOL and a workshop on
proof systems.

I've also been asked recently to request more info and update the
file. Therefore, if it's not much trouble, I'd like to ask you to send
me a short paragraph or two telling me about your interest in HOL, how
you plan to use it, and what features you would like to find in it. If
you'd like to send in an update to previous information too that would
be fine too. I'd really appreciate your input - thanks!


                                                        - Sara