Hi Freek,
Maintaining the numbering of theorems stable (if this is the case) leeds to fossilization of MML. What is the problem in renumbering theorems after moving them around?I would have to edit <http://www.cs.ru.nl/~freek/100/mizar.html> all the time?
You should mention the MML version number anyway. This is very standard, e.g. references to Wikipedia articles should also refer to a particular version, not to "current", as it can change arbitrarily. As for html, at http://mmlquery.mizar.org/mml/ the versions are kept and can be referenced absolutely.
It is a bit of shame that unpacked "raw text" articles are only available for the last version at ftp://mizar.uwb.edu.pl/pub/version. We should keep at least the aricles and abstracts from all versions also available for absolute referencing.
Renumbering all theorems and references in MML after a revision seems like a mundane editorial job._If_ you start to change the numbers on a bigger scale, then _please_ also move the theorems between articles on a much bigger scale, so articles will no longer contain theorems that really should have been somewhere else.
That is one of the ideas behind a wiki for Mizar. I hope it will happen, and not just in the very distant perfect future :-).
One argument that I see in support for avoiding renumbering theorems is that authors get used to numbers of frequently referenced theorems. This does not apply to me;And if one had been working on an article, got distracted, but then tried to pick it up half a year or so later, one would have a bit of a problem, wouldn't you? To get it working again would take much more work then it takes now.
It would work with the old system, and if the article is worth anything, you might get help from Adam & Co. to port it to new version of the system. Surely, if renaming is done on a larger scale, appropriate tools will be more useful/needed than now. Such tools will obviosly be needed also for wiki functionality.
Josef