Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <27500.9405271238@frogland.inmos.co.uk>
Subject: Re: help files for hol90 (fwd)
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Fri, 27 May 1994 13:38:20 +0100 (BST)
Content-Type: text
Content-Length: 1355

Matthew Morley has said:
> -Dear HOL community,
> 
> (recycled)
> 
> -Here to date
> -the only volunteers for the job have been Steve Brackin, myself, and
> -Konrad Slind.  
> 
> Not entirely correct, but let it pass.

? as I wasn't at the last HUG I think this is the first I've heard of
this ... I'll see if I can join in!

> Elsa's "reminder" seems not unwarranted, but I should like to make
> the following observations:
> 
>     The HOL helpfiles display a laudable uniformity of style, so
>     in translating these to reflect hol90's syntax one ought to
>     avoid the temptation to tweak the text at all costs.
> 
>     Phil and collegues have put tremendous effort into the
>     hypertext documentation, but the doc_to_html `script' is
>     non-trivial -- some hand re-touching is inevitable. If there
>     are some `adjustments' we can make to the docs that would
>     minimise the need to hand-code the html versions, it'd be 
>     useful to know in advance. Phil?
> 
>     Note that hol90 introduces record types, delimited by { - },
>     but these have special meaning in the hol88 docs (akin to
>     TeX grouping. So formatting types of functions involving
>     record types needs special care (double up the brackets). 

at the risk of overturning the applecart ... would it make sense to use
HTML the source language now?


DeS