Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <08466-0@swan.cl.cam.ac.uk>; Thu, 2 Apr 1992 20:19:00 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02511; Thu, 2 Apr 92 10:49:32 -0800 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02506; Thu, 2 Apr 92 10:49:26 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <08121-0@swan.cl.cam.ac.uk>; Thu, 2 Apr 1992 19:52:12 +0100 To: shb@oracorp.com Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: LIBRARIES source? In-Reply-To: Your message of Thu, 02 Apr 92 12:40:55 -0500. <9204021740.AA22938@sparta.oracorp.com> Date: Thu, 02 Apr 92 19:52:08 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.123:02.03.92.18.52.15"@cl.cam.ac.uk> > 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? > [... stuff deleted... ] ... I assumed my co-worker just > hadn't obtained that directory because it was large and he didn't think > he'd need it. No, it sounds like you have everything. In particular, LaTeX sources for libraries are supposed to live in the Library directory, and NOT in the Manual directory. Please read Manual/Guide/guide.tex, where all this is explained in detail. Note that not all libraries presently have manuals. In particular, my ind_defs library is documented at present only by the little paper I wrote for last year's HOL user meeting (the proceedings of which has not appeared yet?). This paper therefore temporarily takes the place of a proper library manual for this library. The more_arithmetic and more_lists manuals somehow escaped having Makefiles created for them---this should be fixed by the author of these libraries for version 2.01. Tom