Hi Freek,
So yes, whatever is the mechanism deciding about Mizar changes (I strongly suspect that the mechanism is _you_ :-)Which is the way it should be. Mizar is a such a great system exactly because of this. It gives a unity to the system, and prevents it from "diverging".
I guess all the people behind various LCF descendents would have a bit different opinion about harmfullness of "diverging". Wasn't it John Harrison saying something about liking people to experiment with HOL Light? Wasn't it you, who actually experimented with it by writing another Mizar mode for it? Isn't the Isar "divergence" of Isabelle used pretty much today? Didn't you say that you like George Gonthier's Coq hacks?
I agree that there should be a mechanism for deciding what is "the real Mizar", and also think that the current practice of having Andrzej (and Czeslaw) do that is not bad. But I (obviously) strongly disagree with preventing people to experiment with Mizar and "diverge" from it.
Best, Josef