Re: [mizar] PVS GPLed

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

Josef:

>Even for a (unlabeled) _tree_ there is e.g. the problem
>of hidden arguments (a redefined functor may take some more
>arguments on the semantic level, so there will be additional
>edges in the tree). Or expandable vs. normal types -
>again change already the _tree_ on the semantic level.

Okay, okay, enough already!  I give in!

>And there might be some weird cases even without this,
>e.g. when constructors with the same name are defined for
>several arities ...

I don't think that _that_ will be a problem.  The way I
understand term syntax, this has been taken into account.

Freek