Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, kfisler@cs.indiana.edu
In-Reply-To: <9410101952.AA02414@jaguar.cs.byu.edu> (windley@lal.cs.byu.edu)
Subject: Re: Forwarded message on HOL90 documentation and tutorials
Message-Id: <94Oct10.224054met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 10 Oct 1994 22:40:48 +0100


> We talked about this some at the HOL94 meeting and it now rears its
> ugly head.  Is there any documentation that can help someone *not
> familiar with HOL at all* to get started in HOL90?

The forthcoming release of hol90 has an HTML-based (and much improved
over previous versions, imho) user manual, including a couple of simple
examples. I would suggest checking out the "doc/" directory of the hol90
distribution and also some of the vast array of proofs found in the
system source, for instance those in the "theories/src/" directory of
the distribution. Specific questions posted to this mailing list,
especially by beginners, invariably receive detailed responses.

> (At this point, I need very basic getting started sorts of things.  I
> haven't even been able to figure out how to quit the system without
> manually killing the process.)

Exiting the system is done by exiting SML/NJ, i.e., with ^D.

In essence, hol90 is a great big library built on top of SML/NJ. In
general, a good knowledge of what the SML implementation provides will
raise one's hol90 productivity, so it's worth examining the
documentation that comes with the SML/NJ distribution.

Konrad.