Return-Path: 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 12:39:38 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA06828; Fri, 19 Nov 93 05:22:03 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from [128.232.0.56] by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA06824; Fri, 19 Nov 93 05:21:27 -0700 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 19 Nov 1993 12:18:06 +0000 To: tfm@dcs.gla.ac.uk Cc: info-hol@leopard.cs.byu.edu Subject: Re: hol90 help files In-Reply-To: Your message of "Fri, 19 Nov 93 11:38:16 GMT." <9311191138.AA01424@switha.dcs.gla.ac.uk> Date: Fri, 19 Nov 93 12:17:58 +0000 From: Richard Boulton Message-Id: <"swan.cl.cam.:136270:931119121809"@cl.cam.ac.uk> > 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 Yes, but while people are moving over to HOL90 it may be useful to have documentation describing the anachronistic HOL88 identifiers and perhaps some hint as to how their functionality can be achieved in HOL90. Maybe help files for these identifiers could go in a separate directory from those for identifiers that are actually implemented in HOL90? Richard.