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; Tue, 20 Apr 1993 22:30:30 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17398;
          Tue, 20 Apr 93 14:23:08 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA17393; Tue, 20 Apr 93 14:23:00 -0700
Received: by panther.cs.uidaho.edu id AA20785 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Tue, 20 Apr 1993 14:22:58 -0700
Date: Tue, 20 Apr 1993 14:22:58 -0700
From: Chris Toshok <toshok@panther.cs.uidaho.edu>
Message-Id: <199304202122.AA20785@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Type abbreviations in hol90.5


  Hello all,

  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.

Chris Toshok
toshok@panther.cs.uidaho.edu