Merge pull request #1467 from metamath/rng-to-ring

Rename label fragments 'rng' to 'ring' if they are Ring (NOTE: might create merge conflicts for some unmerged changes)
metamath · Feb 10, 2020 · 59bd588 · 59bd588
2 parents 4e1b5b6 + cb33ff2
commit 59bd588
Show file tree

Hide file tree

Showing 2 changed files with 15,146 additions and 14,904 deletions.
diff --git a/discouraged b/discouraged
diff --git a/set.mm b/set.mm