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

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

On Fri, 8 Mar 2002, Freek Wiedijk wrote:

> >As I understand it, Mizar only has singleton facts.  So
> >probably your proposal number 2 would probably come close to
> >the most desirable behaviour.
>
> Sorry, but I don't understand why you say this.  If Mizar has
> only singleton facts, then proposal 2 should _not_ be the
> one, right, because that is _not_ a singleton fact.  So
> proposal 2 wouldn't fit in the general Mizar style.

What I was trying to say is this: in Isar you always have multiple results
(a "fact" is a "list of theorem" internall).  This means it is no problem
to refer to several previous results simultanously.  This behaviour turns
out as most natural (at least within the Isar framework). In order to get
a similar effect in Mizar, you would have to state explicit conjunctions.

On the other hand, your number 4 (project the last result) is probably
still best for Mizar as it stands.


	Markus

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