Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Wed, 30 Sep 1992 13:50:54 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10477;
          Wed, 30 Sep 92 05:42:26 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA10472;
          Wed, 30 Sep 92 05:42:20 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Wed, 30 Sep 1992 13:40:16 +0100
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: binder inheritance bug.
Date: Wed, 30 Sep 92 13:40:06 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.884:30.08.92.12.41.09"@cl.cam.ac.uk>


The problem with inheritance of binder status from parent theories
has now been solved by a bigfix installed in HOL88 version 2.01.

Anyone who wants to patch their current version of the system can
write to me for the details.

Tom