Re: [mizar] Strong Mizar wish: linking to consider

[Markus Wenzel <wenzelm@informatik.tu-muenchen.de>]

On Sat, 9 Mar 2002, Andrzej Trybulec wrote:

> I must ask somebody to do statistics: how often in MML occurs situation
> when we spare something (a label, a reference) if linking after the
> Choice Statement is allowed.

I don't know any exact numbers, but my general impression is that Mizar
texts tend to be cluttered by more labels than necessary (not just with
"consider").  To get an idea, e.g. see Freek's emerging comparison of the
"N provers of the world", featuring typical entries of Mizar and Isar
texts.


	Markus

--------------------------------------------------------------------
Institut für Informatik, TU München, http://www4.in.tum.de/~wenzelm/
--- <>< ------------------------------------------------------------