Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <m0s8ZLq-000q4xC@radish.research.att.com>
Date: Mon, 8 May 95 16:24 EDT
From: elsa@research.att.com (Elsa Gunter)
To: info-hol@leopard.cs.byu.edu
Subject: renaming things in core hol
Cc: jhr@research.att.com

Dear HOL community:
  In the sml world, there seems to be a move afoot to create an
enlarged standard pervasive environment to be common to most, if not
all, SML compilers/interpreters.  This will allow for a fairly large
library of standard desired functions to be shared among all versions.
This is causing a number of changes which will effect hol90.  One
effect that will hit implementors pretty early is a splitting of the
type of strings into the type of characters and the type of strings.
I have already worked through the hol90 code to accomodate that
change, so users will not feel it in general.  I am also creating a
compatability module to try to ease the process of upgrading, but it
is biased toward encouraging the use of the new system features.
  One problem has threatened to arise that would require a more
visible change to hol90; one that would render it less compatible with
hol88.  In sml, they are planning to expand the collection of
persavive top-level datatypes beyond int, string, real, list, etc., to
include several new ones including an option type with constructors
SOME and NONE (already in SML-NJ), and a sum type with constructors
INL and INR.  The latter poses a problem for hol90, because once a
name is used as a datatype constructor in sml, it can no longer be
used as an indentifier for values.  And as we all know, INL and INR
have been used as identifiers for two theorems in theory "sum" for
quite some time.  The sml people may be willing this time to change
the names of their constructors to accomodate us, but while these
changes are going on, the general problem of such name conflicts may
continue to arise.  I plan to resolve such conflicts by suffixing the
old hol name by _THM or _DEF as is appropriate.  Thus INL would become:

val INL_THM = |- !x. ISL x ==> (INL (OUTL x) = x) : thm

If anybody has reason to disagree with this choice, or feels they have
a better solution, please let me know.
				---Elsa L. Gunter
				   AT&T Bell Labs