Re: [mizar] PVS GPLed

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

Josef:

>>No.  The parse tree will be the same.  The interpretation of
>>the symbols will change, but the parse tree will be the same.
>
>This all depends on the exact definitions of these notions.

I understand what you're saying here.

Still I want to make the point that the _tree_ (as a tree)
will be the same.  The tree structure of the term just
depends on the symbols and their priorities.

However, the constructors that those symbols refer to
obviously _does_ depend on the notations and registrations
that are visible.

Freek