Re: [mizar] Private DB

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

Hi Josef,

>So I'd much rather like to be warned (and stopped) by the system when I 
>write something possibly ambiguous, and forced to rephrase it in readable 
>notation.

You're throwing away the child with the bath water!  Yes, the
behavior of /\ with respect to "Subset of" is less than
perfect, but I'd rather have that, than have nothing like it
at all!  I would hate to have to use different notation to
get /\ have a type of the form "Subset of ..."

Or do I misunderstand what you are saying?

Freek