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; Tue, 11 Jan 1994 17:53:05 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14433;
          Tue, 11 Jan 1994 10:44:17 -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 AA14406;
          Tue, 11 Jan 1994 10:43:42 -0700
Received: from tuminfo2.informatik.tu-muenchen.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA14223;
          Tue, 11 Jan 1994 09:41:27 -0800
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57671>;
          Tue, 11 Jan 1994 18:37:13 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <8097>;
          Tue, 11 Jan 1994 18:36:59 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu
Subject: theories
Message-Id: <94Jan11.183659met.8097@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 11 Jan 1994 18:36:46 +0100


Ralph Reetz notes

> Changing to HOL90.6, I've had the same effect with other theories.
> After building ALL theories anew and using load_library for theories
> like string instead, the problem disappeared. This isn't an explanation,
> but it has helped.

When a new release of hol90 occurs, all user theories need to be rebuilt
on that new version. This is a consequence of the adoption of
timestamps, which makes operations on the theory graph (such as
"new_parent" and "load_theory") secure.

Konrad.