Re: [mizar] Strong Mizar wish: linking to consider (fwd)

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> For instance it might be nice to know what the thesis is,
> when a skeleton step doesn't fit it (actually, because of
> definitions, there probably is a whole list of "expanding"
> theses.)  I often get confused about what the thesis is,
> especially when definitions are involved.  Just knowing that
> I got it wrong is less nice than knowing what it should be.
>
> And if a system prints the thesis in such an error message,
> it would be nice to be able to "copy" the assumption from the
> thesis to put it in an "assume".  Something like that.

I see, a good example. I guess the same goes for Correctness Conditions
and Properties (in the second case I have often trouble, what should be
proved).

Greetings,
Andrzej