Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <14248-0@swan.cl.cam.ac.uk>; Thu, 31 Oct 1991 16:51:48 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA04623;
          Thu, 31 Oct 91 08:33:17 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from electra.oracorp.com by ted.cs.uidaho.edu (15.11/1.34) id AA04619;
          Thu, 31 Oct 91 08:32:21 pst
Date: Thu, 31 Oct 91 11:32:26 EST
From: garrel@com.oracorp.electra
Received: by electra.oracorp.com (4.1/1.3-ORA Corporation) id AA24775;
          Thu, 31 Oct 91 11:32:26 EST
Message-Id: <9110311632.AA24775@electra.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: ploegaer@imec.be's mail of Thu, 31 Oct, 91
Subject: Re: Referring to assumptions by number

ploegaer@imec.be writes:
>
>    oh no ... don't ...
>
>    Please, do *not* use explicit reference to the order of the
>    assumptions...
>    Your code will become unreadable, and which is worse, unportable.
>    In case you do not believe this, read the README file in
>    contrib/v11_lib and stroll throught the related libraries. (or
>    better try to rewrite some of the proofs that broke in v1.12)

Thanks for the advice.  I must say my initial reaction is `Nuts!`, but
I'll think over what you say.  I have read the caveats in The HOL System
Description, and I am not convinced things will be so terrible, at least
for tactics intended for use at the top level of the subgoal package.

Garrel