Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 13 Oct 1994 18:14:50 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA21819; Thu, 13 Oct 1994 11:01:14 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA21815; Thu, 13 Oct 1994 11:01:14 -0600 Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA14672; Thu, 13 Oct 1994 10:55:54 -0600 Message-Id: <9410131655.AA14672@jaguar.cs.byu.edu> To: info-hol@leopard.cs.byu.edu Subject: Forward of message from Kathi Fisler (Two questions from a beginner) Date: Thu, 13 Oct 1994 10:55:52 -0600 From: Phil Windley ------- Forwarded Message From: "Kathi Fisler" Subject: Two questions from a beginner To: info-hol@cs.uidaho.edu (hol) Date: Thu, 13 Oct 1994 10:40:34 -0500 (EST) 1. I am trying to load the arithmetic theory into an interactive HOL session (we're running hol90.6 on a sparcstation). Following the manual, I used add_theory_to_sml, and got the following behavior: - add_theory_to_sml "arithmetic" ; uncaught exception HOL_ERR - I get the same response even when I use the absolute pathname. Is there some environment variable that I need to have set? I tried the theory_path command and it contains theories/ascii but not theories/src. Could that be causing the problem? If so, how can I fix it without rebuilding the system? (I'm not the one who installed it). 2. Is there a list of commands available somewhere? I have figured out the inference rule commands from looking at the proofs in the distribution directories. What I need more are the commands for interacting with HOL, such as the equivalent of the "top_print print_all_thm" command shown in the classic HOL tutorial on the Web. I'm trying to locate the commands by grepping the source files, but that's only of limited effectiveness. Thanks. Kathi - -- Kathi Fisler kfisler@cs.indiana.edu Visual Inference and Hardware Methods Laboratories, Indiana University ------- End of Forwarded Message