Re: [mizar] Hindrances

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

Piotr,

>Yet, there are many obvious cases where the current state of
>MML literally is hindering rather than helping the authors
>and the MML development.

I know this feeling!  I often think "I like the system, but I
don't like the library".  In particular I always feel that
there are much too many "non empty" (or is it "non-empty"?)
attributes everywhere.

Of course there sometimes are non enough "non empty"s.  For
instance, I always have felt that the argument of "Element
of" should have been of type "non empty set" :-)

Freek