Re: [mizar] PVS GPLed

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

Hi Josef,

>I meant some kind of overloading - as a Mizar user, you
>probably know how bad these things sometimes can get :-).

I think the ocaml used in HOL Light is too simple for this
to be a real worry.  And the thm type is too ubiquitous to
be in real danger that someone accidentally will introduce
another datatype with the same name.

>With good coding practices or sufficiently simple system.

Yes, sufficiently simple.

Freek