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 <04716-0@swan.cl.cam.ac.uk>; Thu, 7 May 1992 19:27:32 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12340;
          Thu, 7 May 92 10:03:00 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from eros.uknet.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA12336;
          Thu, 7 May 92 10:02:42 -0700
X400-Received: by mta eros.uknet.ac.uk in /PRMD=UK.AC/ADMD=GOLD 400/C=GB/;
               Relayed; Thu, 7 May 1992 18:02:52 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Thu, 7 May 1992 17:55:06 +0100
Date: Thu, 7 May 1992 17:55:06 +0100
X400-Originator: R.B.Jones@uucp.win0109
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600001455]
X400-Content-Type: P2-1984 (2)
Content-Identifier: 1455
From: R.B.Jones@uucp.win0109
Message-Id: <"1455*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: "discarding theory segments" in ICL HOL

In order to permit the theory hierarchy to be saved in the
PolyML database we found it necessary to implement a system
similar to that described by Tim Leonard.  This has the
advantage that definitions can be deleted without reloading the
entire theory.
              Roger Jones, ICL