Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 6 Dec 1993 04:42:15 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04404;
          Sun, 5 Dec 1993 21:32:13 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA04400;
          Sun, 5 Dec 1993 21:32:08 -0700
Received: from panther.cs.uidaho.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA19121;
          Sun, 5 Dec 1993 20:28:49 -0800
Received: by panther.cs.uidaho.edu id AA19187 (5.65c/IDA-1.4.4 
          for info-hol@cs.uidaho.edu); Sun, 5 Dec 1993 20:27:24 -0800
Date: Sun, 5 Dec 1993 20:27:24 -0800
From: Chris Toshok <toshok@cs.uidaho.edu>
Message-Id: <199312060427.AA19187@panther.cs.uidaho.edu>
To: info-hol@cs.uidaho.edu
Subject: Differences between abs_theory in hol88 and hol90

Hello all,

  I was wondering if anyone had done any work porting hol88 theories that
make use of the abstract theory package.  My problem involves
new_abstract_representation.  This function exists in hol88, but not in the
hol90 port of the package.  I realize that the port was more 
re-engineering than just converting ML to SML, but it seems that specifying
the types associated with an abstract entity, for later retrieval with
abs_type_info.  For that matter, is there any function which does the same
job as abs_type_info in the hol90 port?  Thanks for any and all replies.

Chris Toshok
toshok@cs.uidaho.edu