Shortenings using trpred; extract trom from ordom and further shorten…

…ings. (#4294)
metamath · Oct 16, 2024 · 003b5fd · 003b5fd
1 parent d66ff3a
commit 003b5fd
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 17 deletions.
diff --git a/discouraged b/discouraged
diff --git a/iset.mm b/iset.mm
diff --git a/set.mm b/set.mm