Hi Freek, On Thu, 21 Sep 2006, Freek Wiedijk wrote:
Welcome to this Mizar forum evergreen :-).So is it _always_ me who starts talking about this, or are there other people who find this important? :-)
No, last time it was actually me: http://mizar.uwb.edu.pl/forum/archive/0311/msg00001.html (you have to scroll down, there is a second message from Nov 13 2003 starting that long "weak type" thread - seems to be a bug in the mail html-izing soft).
It started from a need for stating a fairly natural cluster about a parameterized Mizar type, who generally does not have to be non empty for all instantiations of the parameters. I think that after three years that functionality is still pretty much missing (and no, I am not going to write a _new_ system because of that, I want Mizar fixed :-).
Josef