Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Thu, 31 Oct 91 15:35:56-0100
Message-Id: <9110311635.AA05568@esat.kuleuven.ac.be>
From: ploegaer@be.imec
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Referring to assumptions by number


> I seem to remember that, a few weeks back, somebody announced a package
> for referring to assumptions by number, but I have lost the message.
> If I'm not imagining things, I would appreciate hearing from the person
> who announced the package.

   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)

   If you are really interested in this kind of hacks, have a look at
   the library `auxiliary` where you can find everything you want ...
   but DO NOT USE IT (moreover, the "filter tactics" will not be
   supported anymore in the new release of the library)

   people that are not convinced can email me ...

   Wim


PS: Guess most of you know this ... it only is a sign of ultimate
    frustration in my fight with some of the ex-libraries

----------------------------------------------------------------------
Ploegaerts Wim                                e-mail: ploegaer@imec.be
Imec vzw.                                     Tel.:   (32) 16/281 525
Kapeldreef 75                                 Fax.:   (32) 16/281 515
3001   Leuven,  Belgium                       Telex:  26.152