[mizar] cleaning up labels gone awry

[Jesse Alama <alama@stanford.edu>]

I recently finished the "first-draft" formalization of a proof of
Euler's polyhedron formula.  I'm proud of the work I've done, but the
articles that I've written are, well, messy.  The main problem is my use
of labels.  While writing the article, I did not proceed linearly, and
as a result, my labels are often quite out of order.  In proofs, for
example, because of my proof development style I often inserted
statements between two statements, which of course leads to label
problems.

What I'm wondering is what other mizar authors have done to maintain
"label hygiene" in their mizar articles as they write them.  I have some
emacs code that helps me with this (I have a command that allows an
author to insert a new theorem, whose automatically assigned label
depends on the label of the preceding theorem, and, if that newly
generated label is already used, the program goes through the remainder
of the article and "bumps" all labels by one, and modifies references
accordingly), but it doesn't entirely do the job.  What do you do to
keep your articles clean while writing them?

Warm regards,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*496: Too complicated scheme (too many occurrences of a predicate variable)