Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 21 Apr 1993 19:08:33 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20582;
          Wed, 21 Apr 93 10:53:39 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA20577;
          Wed, 21 Apr 93 10:53:27 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57699>;
          Wed, 21 Apr 1993 19:53:12 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8079>;
          Wed, 21 Apr 1993 19:52:59 +0200
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@ted.cs.uidaho.edu
Subject: type abbrevs
Message-Id: <93Apr21.195259met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 21 Apr 1993 19:52:55 +0200


Chris Toshok writes

> How does one go about defining a type abbreviation in hol90?
> in hol88 there is new_type_abbrev, but that function doesn't exist
> in hol90.

Type abbreviations have not been implemented in hol90. Originally this
was due to my laziness, but there are a few other reasons too:

    - as David Shepherd mentioned, you can get nearly the same effect
      with antiquotation. 

    - as David Shepherd mentioned, type abbrevs are not echoed by the 
      prettyprinter.

    - type abbrevs aren't a proper part of a theory, so loading in a
      theory that was built using a type abbrev will not reactivate that
      type abbrev.

    - parameterized type abbrevs seem to be non-trivial to implement
      correctly. (This observation comes from watching Mark Lillibridge
      debug the SML/NJ typechecker last summer.)


Konrad.