Skip to content

Commit

Permalink
Merge branch 'develop' into av-fset3
Browse files Browse the repository at this point in the history
  • Loading branch information
@benjub
benjub authored Sep 23, 2024
2 parents f3dbafc + ff48fe1 commit 2eb9415
Show file tree
Hide file tree
Showing 3 changed files with 1,107 additions and 64 deletions.
3 changes: 2 additions & 1 deletion changes-set.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,8 @@ Date Old New Notes
20-Sep-24 freld [same] moved from GS's mathbox to main set.mm
20-Sep-24 ineqcomi [same] moved from PM's mathbox to main set.mm
20-Sep-24 ineqcom [same] moved from PM's mathbox to main set.mm
20-Sep-24 sylibda sylbida moved from SN's mathbox to main set.mm
18-Sep-24 sylibda sylbida moved from SN's mathbox to main set.mm
17-Sep-24 moel [same] moved from TA's mathbox to main set.mm
16-Sep-24 syl5eqr eqtr3id compare to eqtr3i or eqtr3d
14-Sep-24 iunsn [same] moved from SN's mathbox to main set.mm
10-Sep-24 sspreima [same] moved from TA's mathbox to main set.mm
Expand Down
28 changes: 28 additions & 0 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4923,6 +4923,7 @@
"df-pnf" is used by "mnfnre".
"df-pnf" is used by "pnfex".
"df-pnf" is used by "pnfnre".
"df-prstc" is used by "prstcval".
"df-r" is used by "avril1".
"df-r" is used by "ax1rid".
"df-r" is used by "axresscn".
Expand Down Expand Up @@ -12039,6 +12040,13 @@
"prpssnq" is used by "reclem2pr".
"prpssnq" is used by "suplem1pr".
"prpssnq" is used by "wuncn".
"prstchomval" is used by "prstchom".
"prstchomval" is used by "prstchom2ALT".
"prstchomval" is used by "prstcthin".
"prstcnidlem" is used by "prstchomval".
"prstcnidlem" is used by "prstcnid".
"prstcval" is used by "prstcnidlem".
"prstcval" is used by "prstcthin".
"prub" is used by "genpnnp".
"prub" is used by "ltexprlem6".
"prub" is used by "ltexprlem7".
Expand Down Expand Up @@ -13826,6 +13834,7 @@ New usage of "1lt2pi" is discouraged (1 uses).
New usage of "1ne0sr" is discouraged (1 uses).
New usage of "1nq" is discouraged (9 uses).
New usage of "1nqenq" is discouraged (1 uses).
New usage of "1oexOLD" is discouraged (0 uses).
New usage of "1p1e2apr1" is discouraged (0 uses).
New usage of "1p2e3ALT" is discouraged (0 uses).
New usage of "1pi" is discouraged (11 uses).
Expand Down Expand Up @@ -13864,6 +13873,7 @@ New usage of "2lplnm2N" is discouraged (0 uses).
New usage of "2lplnmN" is discouraged (0 uses).
New usage of "2moex" is discouraged (2 uses).
New usage of "2moswap" is discouraged (1 uses).
New usage of "2oexOLD" is discouraged (0 uses).
New usage of "2pm13.193" is discouraged (3 uses).
New usage of "2pm13.193VD" is discouraged (0 uses).
New usage of "2pmaplubN" is discouraged (1 uses).
Expand Down Expand Up @@ -15466,6 +15476,7 @@ New usage of "df-plpq" is discouraged (3 uses).
New usage of "df-plq" is discouraged (2 uses).
New usage of "df-plr" is discouraged (2 uses).
New usage of "df-pnf" is discouraged (3 uses).
New usage of "df-prstc" is discouraged (1 uses).
New usage of "df-r" is discouraged (6 uses).
New usage of "df-ringcALTV" is discouraged (1 uses).
New usage of "df-rngcALTV" is discouraged (1 uses).
Expand Down Expand Up @@ -16096,6 +16107,7 @@ New usage of "f1coOLD" is discouraged (0 uses).
New usage of "f1cofveqaeqALT" is discouraged (0 uses).
New usage of "f1dmOLD" is discouraged (0 uses).
New usage of "f1eqcocnvOLD" is discouraged (0 uses).
New usage of "f1omoALT" is discouraged (0 uses).
New usage of "f1oweALT" is discouraged (0 uses).
New usage of "f1rhm0to0ALT" is discouraged (0 uses).
New usage of "falnorfalOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -16747,6 +16759,7 @@ New usage of "indistps2ALT" is discouraged (0 uses).
New usage of "indistpsALT" is discouraged (0 uses).
New usage of "indistpsx" is discouraged (0 uses).
New usage of "indpi" is discouraged (1 uses).
New usage of "indthincALT" is discouraged (0 uses).
New usage of "infpssALT" is discouraged (0 uses).
New usage of "int2" is discouraged (3 uses).
New usage of "int3" is discouraged (1 uses).
Expand Down Expand Up @@ -17238,6 +17251,7 @@ New usage of "mobidvALT" is discouraged (0 uses).
New usage of "mobiiOLD" is discouraged (0 uses).
New usage of "moexex" is discouraged (2 uses).
New usage of "moexexv" is discouraged (0 uses).
New usage of "mof0ALT" is discouraged (0 uses).
New usage of "mpjao3danOLD" is discouraged (0 uses).
New usage of "mpofunOLD" is discouraged (0 uses).
New usage of "mpteq12dvOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -17989,6 +18003,10 @@ New usage of "prnmadd" is discouraged (2 uses).
New usage of "prnmax" is discouraged (7 uses).
New usage of "probfinmeasbALTV" is discouraged (0 uses).
New usage of "prpssnq" is discouraged (8 uses).
New usage of "prstchom2ALT" is discouraged (0 uses).
New usage of "prstchomval" is discouraged (3 uses).
New usage of "prstcnidlem" is discouraged (2 uses).
New usage of "prstcval" is discouraged (2 uses).
New usage of "prub" is discouraged (6 uses).
New usage of "psrass1lemOLD" is discouraged (0 uses).
New usage of "psrbagaddclOLD" is discouraged (1 uses).
Expand Down Expand Up @@ -18104,6 +18122,7 @@ New usage of "retbwax1" is discouraged (0 uses).
New usage of "retbwax2" is discouraged (3 uses).
New usage of "retbwax3" is discouraged (0 uses).
New usage of "retbwax4" is discouraged (0 uses).
New usage of "reutruALT" is discouraged (0 uses).
New usage of "rexab2OLD" is discouraged (0 uses).
New usage of "rexbidvALT" is discouraged (0 uses).
New usage of "rexbidvaALT" is discouraged (0 uses).
Expand Down Expand Up @@ -18592,6 +18611,7 @@ New usage of "tendospcanN" is discouraged (1 uses).
New usage of "tfr1ALT" is discouraged (0 uses).
New usage of "tfr2ALT" is discouraged (0 uses).
New usage of "tfr3ALT" is discouraged (0 uses).
New usage of "thincmoALT" is discouraged (0 uses).
New usage of "topnfbey" is discouraged (0 uses).
New usage of "tpid3gVD" is discouraged (0 uses).
New usage of "tratrb" is discouraged (2 uses).
Expand Down Expand Up @@ -18811,6 +18831,7 @@ Proof modification of "19.41rg" is discouraged (58 steps).
Proof modification of "19.41rgVD" is discouraged (127 steps).
Proof modification of "19.43OLD" is discouraged (72 steps).
Proof modification of "1div0apr" is discouraged (77 steps).
Proof modification of "1oexOLD" is discouraged (4 steps).
Proof modification of "1p1e2apr1" is discouraged (7 steps).
Proof modification of "1p2e3ALT" is discouraged (7 steps).
Proof modification of "1t1e1ALT" is discouraged (13 steps).
Expand All @@ -18821,6 +18842,7 @@ Proof modification of "2eu5OLD" is discouraged (81 steps).
Proof modification of "2falsedOLD" is discouraged (14 steps).
Proof modification of "2irrexpqALT" is discouraged (90 steps).
Proof modification of "2logb9irrALT" is discouraged (141 steps).
Proof modification of "2oexOLD" is discouraged (9 steps).
Proof modification of "2pm13.193" is discouraged (91 steps).
Proof modification of "2pm13.193VD" is discouraged (223 steps).
Proof modification of "2sb5nd" is discouraged (125 steps).
Expand Down Expand Up @@ -19572,6 +19594,7 @@ Proof modification of "f1coOLD" is discouraged (99 steps).
Proof modification of "f1cofveqaeqALT" is discouraged (124 steps).
Proof modification of "f1dmOLD" is discouraged (19 steps).
Proof modification of "f1eqcocnvOLD" is discouraged (361 steps).
Proof modification of "f1omoALT" is discouraged (39 steps).
Proof modification of "f1oweALT" is discouraged (805 steps).
Proof modification of "f1rhm0to0ALT" is discouraged (161 steps).
Proof modification of "falimfal" is discouraged (6 steps).
Expand Down Expand Up @@ -19853,6 +19876,7 @@ Proof modification of "incomOLD" is discouraged (37 steps).
Proof modification of "indifdirOLD" is discouraged (147 steps).
Proof modification of "indistps2ALT" is discouraged (43 steps).
Proof modification of "indistpsALT" is discouraged (64 steps).
Proof modification of "indthincALT" is discouraged (202 steps).
Proof modification of "infpssALT" is discouraged (52 steps).
Proof modification of "infregelb" is discouraged (185 steps).
Proof modification of "int2" is discouraged (14 steps).
Expand Down Expand Up @@ -19951,6 +19975,7 @@ Proof modification of "mndoissmgrpOLD" is discouraged (22 steps).
Proof modification of "mo4OLD" is discouraged (9 steps).
Proof modification of "mobidvALT" is discouraged (48 steps).
Proof modification of "mobiiOLD" is discouraged (17 steps).
Proof modification of "mof0ALT" is discouraged (67 steps).
Proof modification of "mpjao3danOLD" is discouraged (29 steps).
Proof modification of "mpofunOLD" is discouraged (95 steps).
Proof modification of "mpteq12dvOLD" is discouraged (18 steps).
Expand Down Expand Up @@ -20077,6 +20102,7 @@ Proof modification of "problem2" is discouraged (104 steps).
Proof modification of "problem3" is discouraged (56 steps).
Proof modification of "problem4" is discouraged (310 steps).
Proof modification of "problem5" is discouraged (133 steps).
Proof modification of "prstchom2ALT" is discouraged (121 steps).
Proof modification of "psrass1lemOLD" is discouraged (1513 steps).
Proof modification of "psrbagaddclOLD" is discouraged (392 steps).
Proof modification of "psrbagconOLD" is discouraged (365 steps).
Expand Down Expand Up @@ -20151,6 +20177,7 @@ Proof modification of "retbwax1" is discouraged (195 steps).
Proof modification of "retbwax2" is discouraged (127 steps).
Proof modification of "retbwax3" is discouraged (20 steps).
Proof modification of "retbwax4" is discouraged (13 steps).
Proof modification of "reutruALT" is discouraged (45 steps).
Proof modification of "rexab2OLD" is discouraged (67 steps).
Proof modification of "rexbidvALT" is discouraged (10 steps).
Proof modification of "rexbidvaALT" is discouraged (10 steps).
Expand Down Expand Up @@ -20302,6 +20329,7 @@ Proof modification of "tdeglem4OLD" is discouraged (703 steps).
Proof modification of "tfr1ALT" is discouraged (19 steps).
Proof modification of "tfr2ALT" is discouraged (52 steps).
Proof modification of "tfr3ALT" is discouraged (84 steps).
Proof modification of "thincmoALT" is discouraged (93 steps).
Proof modification of "topnfbey" is discouraged (75 steps).
Proof modification of "toycom" is discouraged (142 steps).
Proof modification of "tpid3gVD" is discouraged (116 steps).
Expand Down
Loading

0 comments on commit 2eb9415

Please sign in to comment.