Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Mon, 29 Mar 93 05:45:03 -0800
From: val@com.netcom (Dewey Val Schorre)
Message-Id: <9303291345.AA28769@netcom2.netcom.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Beginners Questions


1. The HOL System Reference contains a list of all the Pre-defined ML 
Identifiers. The same information is available by means of the help 
function. This is very useful if I'm trying to read a HOL program that
has been written by someone else. Often, however, I'm trying to write 
a program of my own and I want to find the pre-defined ML identifiers 
that are related to my problem. Is there a list of the Pre-defined ML 
identifers that are grouped together in a logical way?

2. Is there a tactic that will drive negation down? For example, 
it should change the goal

     ~(?x. ((p x) \/ (q x)))

to the goal

	!x. (~(p x) /\ ~(q x))

If there isn't such a tactic, is there something else, maybe some 
derrived rules of inference, that would be useful in writting this 
tactic?

3. Where are 0 and 1 defined. I want to prove ~(0=1).

4. Are that there functions that would list all currently available:

     1) theorems
     2) tactics
     3) conversions
     4) derrived rules of inference

Thanks for any help you can give me.

Val