Skip to content

delete outdated OLD #5140

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wlammen wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

delete outdated OLD #5140

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
77457b8
delete outdated OLD
wlammen Dec 19, 2025
2e8d640
restore accidentially deleted theorems
wlammen Dec 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 0 additions & 57 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9889,8 +9889,6 @@
"mndtcval" is used by "mndtchom".
"moexex" is used by "2moswap".
"moexex" is used by "moexexv".
"mptmpoopabbrdOLDOLD" is used by "mptmpoopabovdOLD".
"mptmpoopabovdOLD" is used by "wksonproplemOLD".
"mpv" is used by "mulcompr".
"mulassnq" is used by "1idpr".
"mulassnq" is used by "addclprlem2".
Expand Down Expand Up @@ -11560,7 +11558,6 @@
"onsetreclem3" is used by "onsetrec".
"opabid" is used by "brabidga".
"opabid" is used by "ssopab2b".
"opabresex2d" is used by "mptmpoopabbrdOLDOLD".
"opelcn" is used by "axicn".
"opelreal" is used by "ax1cn".
"opelreal" is used by "axaddrcl".
Expand Down Expand Up @@ -14249,10 +14246,8 @@ New usage of "ablogrpo" is discouraged (24 uses).
New usage of "ablomuldiv" is discouraged (3 uses).
New usage of "ablonncan" is discouraged (1 uses).
New usage of "ablonnncan1" is discouraged (1 uses).
New usage of "abrexexgOLD" is discouraged (0 uses).
New usage of "abscncfALT" is discouraged (0 uses).
New usage of "abshicom" is discouraged (1 uses).
New usage of "abssdvOLD" is discouraged (0 uses).
New usage of "abvALT" is discouraged (0 uses).
New usage of "ac2" is discouraged (1 uses).
New usage of "ac3" is discouraged (1 uses).
Expand Down Expand Up @@ -15622,7 +15617,6 @@ New usage of "conventions-comments" is discouraged (0 uses).
New usage of "conventions-labels" is discouraged (0 uses).
New usage of "copsexg" is discouraged (1 uses).
New usage of "cotrgOLD" is discouraged (0 uses).
New usage of "cotrgOLDOLD" is discouraged (0 uses).
New usage of "counop" is discouraged (0 uses).
New usage of "crhmsubcALTV" is discouraged (1 uses).
New usage of "cringcALTV" is discouraged (9 uses).
Expand Down Expand Up @@ -15867,14 +15861,10 @@ New usage of "dfdif3OLD" is discouraged (0 uses).
New usage of "dfeu" is discouraged (0 uses).
New usage of "dffr2ALT" is discouraged (0 uses).
New usage of "dffun2OLD" is discouraged (0 uses).
New usage of "dffun2OLDOLD" is discouraged (0 uses).
New usage of "dffun3OLD" is discouraged (0 uses).
New usage of "dffun6OLD" is discouraged (0 uses).
New usage of "dfhnorm2" is discouraged (3 uses).
New usage of "dfid2" is discouraged (0 uses).
New usage of "dfid3" is discouraged (0 uses).
New usage of "dfiop2" is discouraged (3 uses).
New usage of "dfiun2gOLD" is discouraged (0 uses).
New usage of "dfmo" is discouraged (0 uses).
New usage of "dfpjop" is discouraged (4 uses).
New usage of "dfsb1" is discouraged (3 uses).
Expand Down Expand Up @@ -15941,7 +15931,6 @@ New usage of "dif1enOLD" is discouraged (0 uses).
New usage of "dif1enlemOLD" is discouraged (2 uses).
New usage of "dif1ennnALT" is discouraged (0 uses).
New usage of "difidALT" is discouraged (0 uses).
New usage of "difopabOLD" is discouraged (0 uses).
New usage of "dih0bN" is discouraged (0 uses).
New usage of "dih0vbN" is discouraged (0 uses).
New usage of "dih2dimbALTN" is discouraged (0 uses).
Expand Down Expand Up @@ -16052,7 +16041,6 @@ New usage of "dmmulpi" is discouraged (6 uses).
New usage of "dmmulsr" is discouraged (3 uses).
New usage of "dmplp" is discouraged (9 uses).
New usage of "dmrecnq" is discouraged (2 uses).
New usage of "dmxpOLD" is discouraged (0 uses).
New usage of "doca2N" is discouraged (1 uses).
New usage of "doca3N" is discouraged (1 uses).
New usage of "docaclN" is discouraged (2 uses).
Expand Down Expand Up @@ -16354,8 +16342,6 @@ New usage of "elnlfn2" is discouraged (2 uses).
New usage of "elnoOLD" is discouraged (0 uses).
New usage of "elnp" is discouraged (5 uses).
New usage of "elnpi" is discouraged (4 uses).
New usage of "elopabrOLD" is discouraged (0 uses).
New usage of "elopaelxpOLD" is discouraged (0 uses).
New usage of "elovmporab1" is discouraged (0 uses).
New usage of "elpaddatiN" is discouraged (2 uses).
New usage of "elpaddatriN" is discouraged (0 uses).
Expand Down Expand Up @@ -16556,13 +16542,10 @@ New usage of "funcringcsetclem8ALTV" is discouraged (1 uses).
New usage of "funcringcsetclem9ALTV" is discouraged (1 uses).
New usage of "funcrngcsetcALT" is discouraged (0 uses).
New usage of "fundcmpsurinjALT" is discouraged (0 uses).
New usage of "funimaexgOLD" is discouraged (0 uses).
New usage of "funmoOLD" is discouraged (0 uses).
New usage of "funop" is discouraged (2 uses).
New usage of "funopg" is discouraged (0 uses).
New usage of "funopsn" is discouraged (2 uses).
New usage of "fvimacnvALT" is discouraged (0 uses).
New usage of "fvmptopabOLD" is discouraged (0 uses).
New usage of "fvn0fvelrnOLD" is discouraged (0 uses).
New usage of "fvprcALT" is discouraged (0 uses).
New usage of "fvssunirnOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -17208,7 +17191,6 @@ New usage of "ipz" is discouraged (1 uses).
New usage of "isablo" is discouraged (3 uses).
New usage of "isabloi" is discouraged (3 uses).
New usage of "isanmbfmOLD" is discouraged (0 uses).
New usage of "isarep1OLD" is discouraged (0 uses).
New usage of "isass" is discouraged (1 uses).
New usage of "isblo" is discouraged (5 uses).
New usage of "isblo2" is discouraged (1 uses).
Expand Down Expand Up @@ -17289,7 +17271,6 @@ New usage of "iunconnALT" is discouraged (0 uses).
New usage of "iunconnlem2" is discouraged (1 uses).
New usage of "iuneq12dOLD" is discouraged (0 uses).
New usage of "iunidOLD" is discouraged (0 uses).
New usage of "iunopabOLD" is discouraged (0 uses).
New usage of "ivthALT" is discouraged (0 uses).
New usage of "jaoded" is discouraged (1 uses).
New usage of "joincomALT" is discouraged (1 uses).
Expand Down Expand Up @@ -17679,8 +17660,6 @@ 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 "mptmpoopabbrdOLD" is discouraged (0 uses).
New usage of "mptmpoopabbrdOLDOLD" is discouraged (1 uses).
New usage of "mptmpoopabovdOLD" is discouraged (1 uses).
New usage of "mptssALT" is discouraged (0 uses).
New usage of "mpv" is discouraged (1 uses).
New usage of "mrelatglbALT" is discouraged (0 uses).
Expand Down Expand Up @@ -17777,7 +17756,6 @@ New usage of "nfra2" is discouraged (1 uses).
New usage of "nfrab" is discouraged (2 uses).
New usage of "nfral" is discouraged (5 uses).
New usage of "nfrald" is discouraged (2 uses).
New usage of "nfralwOLD" is discouraged (0 uses).
New usage of "nfreu" is discouraged (0 uses).
New usage of "nfreud" is discouraged (1 uses).
New usage of "nfrex" is discouraged (1 uses).
Expand Down Expand Up @@ -18115,7 +18093,6 @@ New usage of "onsetreclem3" is discouraged (1 uses).
New usage of "ontrciOLD" is discouraged (0 uses).
New usage of "onuniorsuciOLD" is discouraged (0 uses).
New usage of "opabid" is discouraged (2 uses).
New usage of "opabresex2d" is discouraged (1 uses).
New usage of "opelcn" is discouraged (1 uses).
New usage of "opelopab4" is discouraged (0 uses).
New usage of "opelreal" is discouraged (8 uses).
Expand Down Expand Up @@ -18477,7 +18454,6 @@ New usage of "qlaxr3i" is discouraged (0 uses).
New usage of "qlaxr4i" is discouraged (0 uses).
New usage of "qlaxr5i" is discouraged (0 uses).
New usage of "quoremnn0ALT" is discouraged (0 uses).
New usage of "r19.21vOLD" is discouraged (0 uses).
New usage of "r19.29OLD" is discouraged (0 uses).
New usage of "r19.29rOLD" is discouraged (0 uses).
New usage of "r19.35OLD" is discouraged (0 uses).
Expand Down Expand Up @@ -18575,7 +18551,6 @@ New usage of "rexeqbidvvOLD" is discouraged (0 uses).
New usage of "rexeqfOLD" is discouraged (0 uses).
New usage of "reximaOLD" is discouraged (0 uses).
New usage of "rexlimddvcbv" is discouraged (0 uses).
New usage of "rexlimivOLD" is discouraged (0 uses).
New usage of "rexlimivaOLD" is discouraged (0 uses).
New usage of "rexlimivwOLD" is discouraged (0 uses).
New usage of "rexor" is discouraged (0 uses).
Expand Down Expand Up @@ -18762,7 +18737,6 @@ New usage of "sbtr" is discouraged (0 uses).
New usage of "sbtrt" is discouraged (1 uses).
New usage of "scandx" is discouraged (12 uses).
New usage of "scmateALT" is discouraged (0 uses).
New usage of "sdom1OLD" is discouraged (0 uses).
New usage of "selsALT" is discouraged (1 uses).
New usage of "sepexlem" is discouraged (1 uses).
New usage of "seq1hcau" is discouraged (0 uses).
Expand Down Expand Up @@ -18984,7 +18958,6 @@ New usage of "sspz" is discouraged (1 uses).
New usage of "ssralv2" is discouraged (2 uses).
New usage of "ssralv2VD" is discouraged (0 uses).
New usage of "ssralvOLD" is discouraged (0 uses).
New usage of "ssrelOLD" is discouraged (0 uses).
New usage of "ssrexvOLD" is discouraged (0 uses).
New usage of "sstr2OLD" is discouraged (0 uses).
New usage of "sstrALT2" is discouraged (0 uses).
Expand Down Expand Up @@ -19219,8 +19192,6 @@ New usage of "w-bnj17" is discouraged (104 uses).
New usage of "w-bnj19" is discouraged (8 uses).
New usage of "watfvalN" is discouraged (1 uses).
New usage of "watvalN" is discouraged (1 uses).
New usage of "wksonproplemOLD" is discouraged (0 uses).
New usage of "wksvOLD" is discouraged (0 uses).
New usage of "wl-embant" is discouraged (0 uses).
New usage of "wl-impchain-a1-1" is discouraged (1 uses).
New usage of "wl-impchain-a1-2" is discouraged (1 uses).
Expand Down Expand Up @@ -19267,7 +19238,6 @@ New usage of "wl-section-impchain" is discouraged (0 uses).
New usage of "wl-section-prop" is discouraged (0 uses).
New usage of "wl-syls1" is discouraged (0 uses).
New usage of "wl-syls2" is discouraged (0 uses).
New usage of "wlkResOLD" is discouraged (0 uses).
New usage of "wvd2" is discouraged (5 uses).
New usage of "wvd3" is discouraged (3 uses).
New usage of "wvhc2" is discouraged (5 uses).
Expand Down Expand Up @@ -19356,9 +19326,7 @@ Proof modification of "a1ii" is discouraged (1 steps).
Proof modification of "ab0ALT" is discouraged (33 steps).
Proof modification of "ab0orvALT" is discouraged (19 steps).
Proof modification of "abid2fOLD" is discouraged (26 steps).
Proof modification of "abrexexgOLD" is discouraged (43 steps).
Proof modification of "abscncfALT" is discouraged (71 steps).
Proof modification of "abssdvOLD" is discouraged (24 steps).
Proof modification of "abvALT" is discouraged (36 steps).
Proof modification of "ackm" is discouraged (71 steps).
Proof modification of "addltmulALT" is discouraged (497 steps).
Expand Down Expand Up @@ -19805,7 +19773,6 @@ Proof modification of "conventions" is discouraged (1 steps).
Proof modification of "conventions-comments" is discouraged (1 steps).
Proof modification of "conventions-labels" is discouraged (1 steps).
Proof modification of "cotrgOLD" is discouraged (99 steps).
Proof modification of "cotrgOLDOLD" is discouraged (110 steps).
Proof modification of "csbcnvgALT" is discouraged (112 steps).
Proof modification of "csbeq2gVD" is discouraged (61 steps).
Proof modification of "csbfv12gALTVD" is discouraged (322 steps).
Expand Down Expand Up @@ -19837,10 +19804,6 @@ Proof modification of "dfdif3OLD" is discouraged (137 steps).
Proof modification of "dfeu" is discouraged (35 steps).
Proof modification of "dffr2ALT" is discouraged (64 steps).
Proof modification of "dffun2OLD" is discouraged (109 steps).
Proof modification of "dffun2OLDOLD" is discouraged (157 steps).
Proof modification of "dffun3OLD" is discouraged (72 steps).
Proof modification of "dffun6OLD" is discouraged (10 steps).
Proof modification of "dfiun2gOLD" is discouraged (131 steps).
Proof modification of "dfmo" is discouraged (44 steps).
Proof modification of "dfsn2ALT" is discouraged (30 steps).
Proof modification of "dftr5OLD" is discouraged (93 steps).
Expand All @@ -19865,7 +19828,6 @@ Proof modification of "dif1enOLD" is discouraged (313 steps).
Proof modification of "dif1enlemOLD" is discouraged (285 steps).
Proof modification of "dif1ennnALT" is discouraged (335 steps).
Proof modification of "difidALT" is discouraged (14 steps).
Proof modification of "difopabOLD" is discouraged (171 steps).
Proof modification of "dih2dimbALTN" is discouraged (450 steps).
Proof modification of "div0OLD" is discouraged (41 steps).
Proof modification of "div11OLD" is discouraged (119 steps).
Expand All @@ -19878,7 +19840,6 @@ Proof modification of "djuexALT" is discouraged (51 steps).
Proof modification of "dmcosseqOLD" is discouraged (167 steps).
Proof modification of "dmfexALT" is discouraged (25 steps).
Proof modification of "dmtrclfvRP" is discouraged (46 steps).
Proof modification of "dmxpOLD" is discouraged (57 steps).
Proof modification of "domnlcanOLD" is discouraged (171 steps).
Proof modification of "domnlcanbOLD" is discouraged (73 steps).
Proof modification of "dral1ALT" is discouraged (34 steps).
Expand Down Expand Up @@ -20091,8 +20052,6 @@ Proof modification of "eliminable3a" is discouraged (7 steps).
Proof modification of "eliminable3b" is discouraged (8 steps).
Proof modification of "elintabOLD" is discouraged (75 steps).
Proof modification of "elnoOLD" is discouraged (66 steps).
Proof modification of "elopabrOLD" is discouraged (58 steps).
Proof modification of "elopaelxpOLD" is discouraged (47 steps).
Proof modification of "elpwgded" is discouraged (23 steps).
Proof modification of "elpwgdedVD" is discouraged (23 steps).
Proof modification of "elrefsymrels3" is discouraged (65 steps).
Expand Down Expand Up @@ -20350,11 +20309,8 @@ Proof modification of "fsumdvdsmulOLD" is discouraged (538 steps).
Proof modification of "fuco11bALT" is discouraged (199 steps).
Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
Proof modification of "funimaexgOLD" is discouraged (133 steps).
Proof modification of "funmoOLD" is discouraged (115 steps).
Proof modification of "fvilbdRP" is discouraged (27 steps).
Proof modification of "fvimacnvALT" is discouraged (102 steps).
Proof modification of "fvmptopabOLD" is discouraged (185 steps).
Proof modification of "fvn0fvelrnOLD" is discouraged (94 steps).
Proof modification of "fvprcALT" is discouraged (26 steps).
Proof modification of "fvssunirnOLD" is discouraged (47 steps).
Expand Down Expand Up @@ -20458,7 +20414,6 @@ Proof modification of "iotaexOLD" is discouraged (57 steps).
Proof modification of "iotassuniOLD" is discouraged (35 steps).
Proof modification of "iotavalOLD" is discouraged (101 steps).
Proof modification of "isanmbfmOLD" is discouraged (15 steps).
Proof modification of "isarep1OLD" is discouraged (106 steps).
Proof modification of "iscmgmALT" is discouraged (57 steps).
Proof modification of "iscsgrpALT" is discouraged (57 steps).
Proof modification of "isdomn2OLD" is discouraged (222 steps).
Expand Down Expand Up @@ -20486,7 +20441,6 @@ Proof modification of "iunconnALT" is discouraged (56 steps).
Proof modification of "iunconnlem2" is discouraged (580 steps).
Proof modification of "iuneq12dOLD" is discouraged (37 steps).
Proof modification of "iunidOLD" is discouraged (77 steps).
Proof modification of "iunopabOLD" is discouraged (117 steps).
Proof modification of "ivthALT" is discouraged (1080 steps).
Proof modification of "jaoded" is discouraged (26 steps).
Proof modification of "jath" is discouraged (318 steps).
Expand Down Expand Up @@ -20570,8 +20524,6 @@ Proof modification of "mobidvALT" is discouraged (48 steps).
Proof modification of "mof0ALT" is discouraged (67 steps).
Proof modification of "mopickr" is discouraged (77 steps).
Proof modification of "mptmpoopabbrdOLD" is discouraged (208 steps).
Proof modification of "mptmpoopabbrdOLDOLD" is discouraged (247 steps).
Proof modification of "mptmpoopabovdOLD" is discouraged (89 steps).
Proof modification of "mptssALT" is discouraged (57 steps).
Proof modification of "mrelatglbALT" is discouraged (66 steps).
Proof modification of "mrelatlubALT" is discouraged (76 steps).
Expand All @@ -20591,7 +20543,6 @@ Proof modification of "nfeu1ALT" is discouraged (25 steps).
Proof modification of "nfinOLD" is discouraged (27 steps).
Proof modification of "nfiu1OLD" is discouraged (28 steps).
Proof modification of "nfopdALT" is discouraged (70 steps).
Proof modification of "nfralwOLD" is discouraged (27 steps).
Proof modification of "nfunOLD" is discouraged (37 steps).
Proof modification of "nfunidALT" is discouraged (33 steps).
Proof modification of "nfunidALT2" is discouraged (49 steps).
Expand Down Expand Up @@ -20658,7 +20609,6 @@ Proof modification of "onfrALTlem5" is discouraged (320 steps).
Proof modification of "onfrALTlem5VD" is discouraged (320 steps).
Proof modification of "ontrciOLD" is discouraged (9 steps).
Proof modification of "onuniorsuciOLD" is discouraged (16 steps).
Proof modification of "opabresex2d" is discouraged (48 steps).
Proof modification of "opelopab4" is discouraged (69 steps).
Proof modification of "opidon2OLD" is discouraged (80 steps).
Proof modification of "opidonOLD" is discouraged (198 steps).
Expand Down Expand Up @@ -20713,7 +20663,6 @@ Proof modification of "pzriprng1ALT" is discouraged (534 steps).
Proof modification of "pzriprngALT" is discouraged (150 steps).
Proof modification of "qexALT" is discouraged (64 steps).
Proof modification of "quoremnn0ALT" is discouraged (360 steps).
Proof modification of "r19.21vOLD" is discouraged (60 steps).
Proof modification of "r19.29OLD" is discouraged (39 steps).
Proof modification of "r19.29rOLD" is discouraged (39 steps).
Proof modification of "r19.35OLD" is discouraged (72 steps).
Expand Down Expand Up @@ -20790,7 +20739,6 @@ Proof modification of "rexeqOLD" is discouraged (11 steps).
Proof modification of "rexeqbidvvOLD" is discouraged (47 steps).
Proof modification of "rexeqfOLD" is discouraged (55 steps).
Proof modification of "reximaOLD" is discouraged (68 steps).
Proof modification of "rexlimivOLD" is discouraged (23 steps).
Proof modification of "rexlimivaOLD" is discouraged (13 steps).
Proof modification of "rexlimivwOLD" is discouraged (14 steps).
Proof modification of "rexssOLD" is discouraged (44 steps).
Expand Down Expand Up @@ -20863,7 +20811,6 @@ Proof modification of "sbsbc" is discouraged (21 steps).
Proof modification of "sbtALT" is discouraged (12 steps).
Proof modification of "sbtT" is discouraged (7 steps).
Proof modification of "scmateALT" is discouraged (236 steps).
Proof modification of "sdom1OLD" is discouraged (73 steps).
Proof modification of "selsALT" is discouraged (34 steps).
Proof modification of "sgrpplusgaopALT" is discouraged (82 steps).
Proof modification of "sii" is discouraged (145 steps).
Expand Down Expand Up @@ -20909,7 +20856,6 @@ Proof modification of "sspwtrALT2" is discouraged (72 steps).
Proof modification of "ssralv2" is discouraged (83 steps).
Proof modification of "ssralv2VD" is discouraged (147 steps).
Proof modification of "ssralvOLD" is discouraged (23 steps).
Proof modification of "ssrelOLD" is discouraged (198 steps).
Proof modification of "ssrexvOLD" is discouraged (23 steps).
Proof modification of "sstr2OLD" is discouraged (49 steps).
Proof modification of "sstrALT2" is discouraged (81 steps).
Expand Down Expand Up @@ -21054,8 +21000,6 @@ Proof modification of "vtoclegftOLD" is discouraged (50 steps).
Proof modification of "vtoclfOLD" is discouraged (28 steps).
Proof modification of "vtoclgOLD" is discouraged (25 steps).
Proof modification of "vtxdusgr0edgnelALT" is discouraged (94 steps).
Proof modification of "wksonproplemOLD" is discouraged (278 steps).
Proof modification of "wksvOLD" is discouraged (81 steps).
Proof modification of "wl-cases2-dnf" is discouraged (85 steps).
Proof modification of "wl-dfclab" is discouraged (73 steps).
Proof modification of "wl-embant" is discouraged (12 steps).
Expand Down Expand Up @@ -21103,7 +21047,6 @@ Proof modification of "wl-section-impchain" is discouraged (1 steps).
Proof modification of "wl-section-prop" is discouraged (1 steps).
Proof modification of "wl-syls1" is discouraged (12 steps).
Proof modification of "wl-syls2" is discouraged (14 steps).
Proof modification of "wlkResOLD" is discouraged (50 steps).
Proof modification of "xpexgALT" is discouraged (84 steps).
Proof modification of "xpfiOLD" is discouraged (373 steps).
Proof modification of "xrge0tmdALT" is discouraged (166 steps).
Expand Down
Loading