minor corrections to #4284 (#4295)

metamath · Oct 16, 2024 · 756f7f0 · 756f7f0
1 parent 003b5fd
commit 756f7f0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 7 deletions.
diff --git a/discouraged b/discouraged
diff --git a/set.mm b/set.mm