Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Thu, 2 Apr 92 12:40:55 EST
From: shb@oracorp.com
Message-Id: <9204021740.AA22938@sparta.oracorp.com>
To: info-hol@ted.cs.uidaho.edu
Subject: LIBRARIES source?

I sent the following note, and even received a reply to it, but
MAILER-DAEMON@ted.cs.uidaho.edu sent it back with a "Can't create
output" error message so I'll submit it again on the chance that that
will be useful.  The reply I got also indicated that I need to supply
more information, so I've added another paragraph giving it.

How can I obtain an on-line copy of the source for the LIBRARIES
document for HOL88 2.0?  Also, am I correct in assuming that this
document supersedes all the text included in the individual
hol/Library subdirectories?

I have Manual, Training, and help documentation directories for HOL88
2.0 that one of my coworkers got somewhere, and the Libraries
subdirectory under Manual contains a Makefile with a command giving a
"make all" command in the Manual subdirectory of each library entry
that has documentation.  The list of subdirectories that have
documentation includes ind_defs, more_arithmetic, and more_lists, even
though my hol/Library subdirectories for them don't have Makefiles.
The default path to the library documentation in the Makefile also
referred to a Library directory that would have been a sibling of the
Manual, Training, and help directories, so I assumed my co-worker just
hadn't obtained that directory because it was large and he didn't think
he'd need it.

Steve Brackin
ORA Corporation
Ithaca, NY