Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu
Subject: hol90 help files
Message-Id: <93Nov19.010123met.8087@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 19 Nov 1993 01:01:20 +0100


Some ML identifiers that occur in hol88 do not occur in hol90. These
fall into 3 rough categories: anachronisms, renamings, and omissions.

    1. Anachronism. This is a function entirely peculiar to hol88, such
       as the "lisp" function. I would suggest adding a \COMMENT field
       saying "Anachronism".

    2. Renaming. This is a function in hol88 that has an equal in hol90;
       it just has a different name. Sometimes, a whole group of
       functions need to be renamed, such as those for prettyprinting.
       One example is "tty_read" in hol88; its hol90 equivalent is
       "IO.output". Again, I would suggest adding a \COMMENT field
       noting its renaming.  

    3. Omissions. There are a very few functions in hol88 that are not,
       but should be, in hol88. Yet again, I suggest adding a suitable
       \COMMENT field. 

All the identifiers in hol88 but not hol90 have already been loosely
categorized in the above fashion. This information is available by doing
a

     help "hol88_extras";

or the equivalent in xholhelp. It will make your job a lot easier to
check this listing before starting on a translation.


Konrad.