Return-Path: 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 17:01:55 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20015; Wed, 21 Apr 93 08:45:54 -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 AA20010; Wed, 21 Apr 93 08:45:38 -0700 Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <57693>; Wed, 21 Apr 1993 17:45:08 +0200 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57717>; Wed, 21 Apr 1993 15:49:44 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8081>; Wed, 21 Apr 1993 15:42:24 +0200 From: Konrad Slind To: toshok@panther.cs.uidaho.edu In-Reply-To: Chris Toshok's message of Tue, 20 Apr 1993 23:22:58 +0200 <199304202122.AA20785@panther.cs.uidaho.edu> Subject: Type abbreviations in hol90.5 Message-Id: <93Apr21.154224met_dst.8081@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 21 Apr 1993 15:42:17 +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. - 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. - as David Shepherd mentioned, type abbrevs are not echoed by the prettyprinter. - 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.