Re: [mizar] Reference distances?

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

Thanks for all your help with this.

>This proposition is hidden from the Mizar author - he cannot quote it, but 
>it is present as a regular proposition in Mizar and in MPTP, so MPTP gives 
>it a name (e3) too. The quotable propositions A3 and A4 are "justified" by 
>this proposition, and they come right after it, so their MPTP names are 
>"e4" and "e5".

Aha!  So when I am counting the "distance", I'd prefer to
_not_ have this "e3" increase the distance.  Is there an easy
way to somehow take this into account?  Is there an easy way
to find out which of "your" labels are "quotable" and which
ones are not?

Freek