Rename syl5bi to biimtrid in iset.mm

metamath · Jan 11, 2025 · 14628d7 · 14628d7
1 parent e1c1548
commit 14628d7
Show file tree

Hide file tree

Showing 2 changed files with 1,975 additions and 1,972 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -70,7 +70,6 @@ proposed  syl5com   imtridcom
 proposed  syl5      imtrid      alternate proposal: sylid
 proposed  syl56     imtridi
 proposed  syl5d     imtridd
-underway  syl5bi    biimtrid
 proposed  syl5bir   biimtrrid
 proposed  syl5ib    imbitrid
 proposed  syl5ibcom imbitridcom
@@ -88,10 +87,10 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+10-Jan-25 syl5bi    biimtrid
  9-Jan-25 fvresval  [same]      Moved from SF's mathbox to main set.mm
  9-Jan-25 brtp      [same]      Moved from SF's mathbox to main set.mm
  9-Jan-25 ---       ---         Moved initial surreal definitions from
-                                SF's mathbox to main set.mm
  9-Jan-25 nfrexdg   nfrexd      consistent with nfrald
  9-Jan-25 nfrexg    nfrex       consistent with nfral
  7-Jan-25 rhmdvdsr  [same]      Moved from TA's mathbox to main set.mm