Date: Sat, 27 Apr 91 10:04:38 BST
From: Mike Gordon <mjcg%com.sri.cam@com.sri.ai>
Message-Id: <9104270904.AA04968@harlech.cam.sri.com>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: Phil Windley's message of Thu, 25 Apr 91 17:59:02 PDT <9104260059.AA14977@panther.cs.uidaho.edu>
Subject: save_thm problem


Phil Windley's the save_thm problem is the result of a
"rationalization" of HOL! We will look into what should be done.
Ideally, I hope we can restore the saving of hypotheses (since the
formal definition suggests it should be possible). If it turns out
that there are strong reasons for having the primitive not save
hypotheses, then we can provide a derived tool that does support it
(by encoding theorems with hypothesis by ones without). Such a hack
was present in Version 1.11 via the (subsequently deleted)
"IS_ASSUMPTION_OF" hack.

If there are any other beloved features of HOL that you find missing
in Version 1.12 please let us know. We deleted a lot of historical
relics and ML functions that were not intended for general use.
However, it is possible that we inadvertently got rid of too much.
The goal is to make HOL smaller and more rational (and hence easier to
fully document and maintain). The next release of the system will aim
to correct anomalies with Version 1.12.

Mike