Re: [mizar] Reference distances?

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hi Freek,

On Sun, 5 Feb 2006, Freek Wiedijk wrote:

> 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.

Maybe my answer is out of your question, but in an "ideal" case such a
proof should not appear. It should look like:

proof
  assume that
A1: ... and
A2: ...;
  ex ... st ... & ... by ...;
  hence ... by ...;
end;

where you have two labels and two justifications.

Best regards
Artur