Rename label fragments 'rng' to 'ring' if they are Ring
Rename label fragments 'rng' to 'ring' if they are Ring

NOTE: Because this renames a lot of labels and then rewraps,
most external changes will *NOT* merge cleanly with this.
If you have a not-yet-merged change, it needs to first
apply the renames on this branch, then rewrap.

This commit implments the rename of label fragments from 'rng' to 'ring'
when they involve a Ring, per:
https://github.com/metamath/set.mm/issues/1389

This also provides a useful test/demo of our scripts to enable
mass renames. These scripts provide a mechanism so we *can*
rename labels in a safer and more automated way.

These renames were developed by using an improved
"scripts/rename-proposals", reviewed, and then applied with an improved
"scripts/mass-rename".  The proposed script improvements have been
submitted as a separate commit (they are not in this one).

Signed-off-by: David A. Wheeler <9ae72d22d8b894b865a7a496af4fab6320e6abb2@dwheeler.com>

metamath/set.mm,metamath/set.mm,metamath/set.mm