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, 19 Nov 1993 11:59:19 +0000
Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA06731;
          Fri, 19 Nov 93 04:41:06 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.7/16.2) id AA06727; Fri, 19 Nov 93 04:40:26 -0700
Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <23025-0@goggins.dcs.gla.ac.uk>;
          Fri, 19 Nov 1993 11:38:27 +0000
Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA01424;
          Fri, 19 Nov 93 11:38:17 GMT
From: tfm@dcs.gla.ac.uk
Message-Id: <9311191138.AA01424@switha.dcs.gla.ac.uk>
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: hol90 help files
In-Reply-To: Your message of "Fri, 19 Nov 93 01:01:20 +0100." <93Nov19.010123met.8087@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 19 Nov 93 11:38:16 +0000


> Some ML identifiers that occur in hol88 do not occur in hol90. These
> fall into 3 rough categories: anachronisms, renamings, and omissions.
> ...
> ...       as the "lisp" function. I would suggest adding a \COMMENT field
>           saying "Anachronism".
> ...
> ... etc

Huh?  So why not just *not* have help files for these functions 
in the hol90 version of the documentation?   To attempt to have 
a single set of help files for both systems seems unwise.

Tom