Reduce ax-13 usage by adding dv conditions (#3781)

* reduced ax-13 usage * more accurate comment * comment correction * converted *ALT suffix into *g * comment correction * updated changes-set.txt --------- Co-authored-by: tirix <[email protected]>
metamath · Jan 25, 2024 · 259bd9b · 259bd9b
1 parent c5050ab
commit 259bd9b
Show file tree

Hide file tree

Showing 3 changed files with 252 additions and 125 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -80,6 +80,21 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 23-Jan-24 nelb      [same]      moved from TA's mathbox to main set.mm
+20-Jan-24 nfiund    nfiundg
+20-Jan-24 bnj1441   bnj1441g
+20-Jan-24 cbviinv   cbviinvg
+20-Jan-24 cbviunv   cbviunvg
+20-Jan-24 cbviin    cbviing
+20-Jan-24 cbviun    cbviung
+20-Jan-24 nfiin     nfiing
+20-Jan-24 nfiun     nfiung
+20-Jan-24 nfrex     nfrexg
+20-Jan-24 nfrexd    nfrexdg
+20-Jan-24 nfaba1    nfaba1g
+20-Jan-24 nfab      nfabg
+20-Jan-24 hblem     hblemg
+20-Jan-24 nfsab     nfsabg
+20-Jan-24 hbab      hbabg 
 17-Jan-24 mteqand   [same]      moved from SN's mathbox to main set.mm
 15-Jan-24 sseqtr4d  sseqtrrd
 14-Jan-24 sseqtr4i  sseqtrri

diff --git a/discouraged b/discouraged
@@ -13813,6 +13813,7 @@ New usage of "bnj1423" is discouraged (1 uses).
 New usage of "bnj1424" is discouraged (2 uses).
 New usage of "bnj1436" is discouraged (12 uses).
 New usage of "bnj1441" is discouraged (0 uses).
+New usage of "bnj1441g" is discouraged (0 uses).
 New usage of "bnj1442" is discouraged (1 uses).
 New usage of "bnj1444" is discouraged (1 uses).
 New usage of "bnj1445" is discouraged (1 uses).