Re: [mizar] Reference distances?

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

Hi Josef,

>But there is no difference between them and the lemmas proved at lower 
>blocks in Mizar, look e.g. at the beginning of CARD_1:
>http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html.937/card_1.html - it's a 
>non-theorem top-level lemma, used in other proofs. I am not happy with 
>this, but such lemmas may even contain local constants if such constants 
>are introduced at the top-level block (e.g. by (re)considering).

Yes, I know all this.  But I am not able to measure the
"distance" of the references to theorems from other articles,
and _most_ of the "top level" references seem to me of a
similar kind.  So I thought I should treat them similarly,
i.e., ignore them.

One more question: can you clarify the outcome of the "sed"
command you mentioned to me?  For instance, suppose that I
have a proof:

  proof
   assume
A1: ... and
A2: ...;
   consider ... such that
A3: ... and
A4: ... by ...;
   thus
A5: ... by ...;
  end;

Then I have five labels, but only two justifications.  So
what would the structure of the output of the sed command
that you gave be like in this case.  Would it have two
lines?  Or five?  Or seven?

(I could try to find proofs like this in the library and look
at what actually happens there, but maybe it becomes clearer
if you explain it.)

Freek