Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 24 Sep 1993 15:01:47 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA29554;
          Fri, 24 Sep 93 06:48:08 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from scylla.oracorp.com by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA29550; Fri, 24 Sep 93 06:47:26 -0700
Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) 
          id AA21715; Fri, 24 Sep 93 09:46:42 EDT
Date: Fri, 24 Sep 93 09:46:36 EDT
From: shb@oracorp.com
Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA11970;
          Fri, 24 Sep 93 09:46:36 EDT
Message-Id: <9309241346.AA11970@sparta.oracorp.com>
To: info-hol@cs.uidaho.edu
Subject: C/HOL90 communication

What's the simplest and/or most robust technique people can suggest
for having a C program find out whether a particular theorem is in a
HOL90 theory?  One can assume that if the theorem is present then it
has a name known to the C program, if that helps.

Steve Brackin
ORA