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

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

Dear Andrzej,

>> The Mizar checker mizf doesn't need to care about this,
>> because all it ever prints is error numbers.  But if you want
>> a system that prints more information than that (most systems
>> do, and I expect HELM = MoWGLI wants be one of them), then
>> this might be a problem.  If you don't mind the "output" not
>> to be usable as "input" again, there's no reason to worry.
>> But _I_ like to be able to occasionally cut-paste stuff back
>> into my source files.
>
>Could you give an example.

Of why I would like a system to print more than just error
numbers, and why I would like to be able to take part of such
output and use it in my article?

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.

Freek