Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <13069-0@swan.cl.cam.ac.uk>; Mon, 13 Apr 1992 17:27:47 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14206;
          Mon, 13 Apr 92 09:11:10 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA14202;
          Mon, 13 Apr 92 09:11:00 -0700
Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <12754-0@swan.cl.cam.ac.uk>; Mon, 13 Apr 1992 17:08:52 +0100
To: "Tim Leonard, DTN 225-5809, HLO2-3/C11 13-Apr-1992 1126" <leonard@com.dec.enet.ricks>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: A wordn library.
In-Reply-To: Your message of Mon, 13 Apr 92 11:25:04 -0400. <9204131525.AA14974@easynet.crl.dec.com>
Date: Mon, 13 Apr 92 17:08:47 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.757:13.03.92.16.08.55"@cl.cam.ac.uk>


Tim Leonard writes:

  o Allow datatypes to be named something other than word<n>.  For example,
    I use ": word1", but I call it ": bit", and I use ": word8", but I call
    it ": byte".  Since different users will want to use different names, the
    names should be supplied by the user.  I changed the wordn code to allow
    the user to supply a name.  (I'd guess this would be much better done as
    part of abstract theories, but that's way beyond me.)  The change was
    trivial except that now there isn't a canonical name for the conversion
    routines, which is a slight pain.

An alternative is to use "new_type_abbrev" to set up your own type name,
although this has the disadvantage of not being stored in theory files.

John.