Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 20 Jan 1995 18:28:37 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA02448;
          Fri, 20 Jan 1995 11:15:42 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA02443;
          Fri, 20 Jan 1995 11:15:40 -0700
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Fri, 20 Jan 1995 18:12:27 +0000
To: info-hol@leopard.cs.byu.edu
Cc: tfm@dcs.gla.ac.uk
Subject: Standard library directory structure.
Date: Fri, 20 Jan 1995 18:11:17 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:296240:950120182934"@cl.cam.ac.uk>

I noticed recently that the HOL88 libraries almost universally
fail to conform to the section in the Author's Guide to Writing 
HOL Documentation that stipulates a standard directory organization
for the help files of a HOL library.  (See item 3 in section 8.1.)
Would anyone object if, in the next release, we actually imposed this
standard on the existing libraries?  It would make it much easier to
construct help file browsers that can know about libraries.

All objections by email to me, please.

Tom