Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 29 Mar 1993 17:07:15 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28869; Mon, 29 Mar 93 07:42:40 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from [129.215.160.108] by ted.cs.uidaho.edu (16.6/1.34) id AA28864; Mon, 29 Mar 93 07:42:21 -0800 Received: from burra.dcs.ed.ac.uk by dcs.ed.ac.uk id aa05956; 29 Mar 93 15:37 GMT To: Dewey Val Schorre Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Beginners Questions In-Reply-To: Your message of "Mon, 29 Mar 93 15:28:36 BST." <"swan.cl.ca.578:29.03.93.14.29.08"@cl.cam.ac.uk> Date: Mon, 29 Mar 93 16:37:38 BST From: Matthew Morley Message-Id: <9303291537.aa05956@dcs.ed.ac.uk> -> 4. Are that there functions that would list all currently available: -> -> 1) theorems -> 2) tactics -> 3) conversions -> 4) derrived rules of inference - -I'm afraid not, but again see Wai Wong's useful summary. - If you have it, Sara Kalvala's xholhelp will do this for you, up to a point. E.g. to list all known theorems in the search path leave the dialogue box empty and click on "theorems" button. Sim. "apropos" but be prepared to wait a while. You can search for patterns, like *TAC to get at all things called somethingTAC, but not necessarily all tactics! You might tailor HOL_HELP_PATH & THM_HELP_PATH to access contributed and other library documentation too. The version of this program released with hol90.5 makes this a little easier, I hope. Matthew