delete outdated OLD theorems (#5002)

Author: wlammen

discouraged

@@ -14568,7 +14568,6 @@ 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 "abn0OLD" is discouraged (0 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).
@@ -15834,9 +15833,6 @@ New usage of "chub2i" is discouraged (24 uses).
 New usage of "chunssji" is discouraged (0 uses).
 New usage of "chvar" is discouraged (2 uses).
 New usage of "chvarv" is discouraged (0 uses).
-New usage of "clel2gOLD" is discouraged (0 uses).
-New usage of "clel4OLD" is discouraged (0 uses).
-New usage of "clelabOLD" is discouraged (0 uses).
 New usage of "cleljustALT" is discouraged (0 uses).
 New usage of "cleljustALT2" is discouraged (0 uses).
 New usage of "clelsb1f" is discouraged (0 uses).
@@ -15958,7 +15954,6 @@ New usage of "con5i" is discouraged (2 uses).
 New usage of "conventions" is discouraged (0 uses).
 New usage of "conventions-comments" is discouraged (0 uses).
 New usage of "conventions-labels" is discouraged (0 uses).
-New usage of "copsex2gOLD" 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).
@@ -17542,7 +17537,6 @@ New usage of "in2" is discouraged (36 uses).
 New usage of "in2an" is discouraged (1 uses).
 New usage of "in3" is discouraged (13 uses).
 New usage of "in3an" is discouraged (1 uses).
-New usage of "indifdirOLD" is discouraged (0 uses).
 New usage of "indistps2ALT" is discouraged (0 uses).
 New usage of "indistpsALT" is discouraged (0 uses).
 New usage of "indistpsALTOLD" is discouraged (0 uses).
@@ -17556,8 +17550,6 @@ New usage of "int2" is discouraged (3 uses).
 New usage of "int3" is discouraged (1 uses).
 New usage of "intidOLD" is discouraged (0 uses).
 New usage of "intnatN" is discouraged (0 uses).
-New usage of "intprOLD" is discouraged (0 uses).
-New usage of "intprgOLD" is discouraged (0 uses).
 New usage of "inxpOLD" is discouraged (0 uses).
 New usage of "iorlid" is discouraged (2 uses).
 New usage of "iotaeq" is discouraged (0 uses).
@@ -18161,7 +18153,6 @@ New usage of "nfae" is discouraged (21 uses).
 New usage of "nfald2" is discouraged (6 uses).
 New usage of "nfccdeq" is discouraged (0 uses).
 New usage of "nfcdeq" is discouraged (1 uses).
-New usage of "nfceqdfOLD" is discouraged (0 uses).
 New usage of "nfcrALT" is discouraged (0 uses).
 New usage of "nfcsb" is discouraged (5 uses).
 New usage of "nfcsbd" is discouraged (1 uses).
@@ -18895,7 +18886,6 @@ New usage of "preleqALT" is discouraged (0 uses).
 New usage of "prfiALT" is discouraged (0 uses).
 New usage of "prlem934" is discouraged (3 uses).
 New usage of "prlem936" is discouraged (1 uses).
-New usage of "prmdvdssqOLD" is discouraged (0 uses).
 New usage of "prmgaplcm" is discouraged (0 uses).
 New usage of "prmgapprmo" is discouraged (0 uses).
 New usage of "prn0" is discouraged (8 uses).
@@ -18962,7 +18952,6 @@ New usage of "rabeqcOLD" is discouraged (0 uses).
 New usage of "rabexgOLD" is discouraged (0 uses).
 New usage of "rabid2OLD" is discouraged (0 uses).
 New usage of "rabrabiOLD" is discouraged (0 uses).
-New usage of "ral0OLD" is discouraged (0 uses).
 New usage of "ralabOLD" is discouraged (0 uses).
 New usage of "ralbidaOLD" is discouraged (0 uses).
 New usage of "ralcom13OLD" is discouraged (0 uses).
@@ -18972,8 +18961,6 @@ New usage of "ralcom4OLD" is discouraged (0 uses).
 New usage of "raleleqOLD" is discouraged (0 uses).
 New usage of "raleqOLD" is discouraged (0 uses).
 New usage of "raleqbidvvOLD" is discouraged (0 uses).
-New usage of "ralf0OLD" is discouraged (0 uses).
-New usage of "ralidmOLD" is discouraged (0 uses).
 New usage of "ralimaOLD" is discouraged (0 uses).
 New usage of "ralprgOLD" is discouraged (0 uses).
 New usage of "ralrexbidOLD" is discouraged (0 uses).
@@ -19071,7 +19058,6 @@ 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 "rexn0OLD" is discouraged (0 uses).
 New usage of "rexor" is discouraged (0 uses).
 New usage of "rexprgOLD" is discouraged (0 uses).
 New usage of "rexrnmpt" is discouraged (0 uses).
@@ -19659,8 +19645,6 @@ New usage of "unexbOLD" is discouraged (0 uses).
 New usage of "unexgOLD" is discouraged (0 uses).
 New usage of "unierri" is discouraged (0 uses).
 New usage of "unifndx" is discouraged (8 uses).
-New usage of "uniprOLD" is discouraged (0 uses).
-New usage of "uniprgOLD" is discouraged (0 uses).
 New usage of "unipwr" is discouraged (0 uses).
 New usage of "unipwrVD" is discouraged (0 uses).
 New usage of "unisnALT" is discouraged (0 uses).
@@ -19741,7 +19725,6 @@ New usage of "vd03" is discouraged (2 uses).
 New usage of "vd12" is discouraged (9 uses).
 New usage of "vd13" is discouraged (3 uses).
 New usage of "vd23" is discouraged (3 uses).
-New usage of "vexOLD" is discouraged (0 uses).
 New usage of "vfermltlALT" is discouraged (0 uses).
 New usage of "vk15.4j" is discouraged (0 uses).
 New usage of "vk15.4jVD" is discouraged (0 uses).
@@ -19755,7 +19738,6 @@ New usage of "vtocl3gaOLDOLD" is discouraged (0 uses).
 New usage of "vtocl3gafOLD" is discouraged (0 uses).
 New usage of "vtocl4gaOLD" is discouraged (0 uses).
 New usage of "vtoclOLD" is discouraged (0 uses).
-New usage of "vtocldOLD" is discouraged (0 uses).
 New usage of "vtocleOLD" is discouraged (0 uses).
 New usage of "vtoclegftOLD" is discouraged (0 uses).
 New usage of "vtoclfOLD" is discouraged (0 uses).
@@ -19956,7 +19938,6 @@ Proof modification of "ab0ALT" is discouraged (33 steps).
 Proof modification of "ab0OLD" is discouraged (146 steps).
 Proof modification of "ab0orvALT" is discouraged (19 steps).
 Proof modification of "abid2fOLD" is discouraged (26 steps).
-Proof modification of "abn0OLD" is discouraged (28 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).
@@ -20372,9 +20353,6 @@ Proof modification of "cffldtocusgrOLD" is discouraged (165 steps).
 Proof modification of "cflemOLD" is discouraged (136 steps).
 Proof modification of "cgsex4gOLD" is discouraged (318 steps).
 Proof modification of "chordthmALT" is discouraged (440 steps).
-Proof modification of "clel2gOLD" is discouraged (30 steps).
-Proof modification of "clel4OLD" is discouraged (24 steps).
-Proof modification of "clelabOLD" is discouraged (75 steps).
 Proof modification of "cleljustALT" is discouraged (25 steps).
 Proof modification of "cleljustALT2" is discouraged (25 steps).
 Proof modification of "clelsb2OLD" is discouraged (63 steps).
@@ -20423,7 +20401,6 @@ Proof modification of "con5i" is discouraged (13 steps).
 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 "copsex2gOLD" is discouraged (119 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).
@@ -21112,7 +21089,6 @@ Proof modification of "in2" is discouraged (10 steps).
 Proof modification of "in2an" is discouraged (18 steps).
 Proof modification of "in3" is discouraged (12 steps).
 Proof modification of "in3an" is discouraged (21 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 "indistpsALTOLD" is discouraged (64 steps).
@@ -21124,8 +21100,6 @@ Proof modification of "infsdomnnOLD" is discouraged (39 steps).
 Proof modification of "int2" is discouraged (14 steps).
 Proof modification of "int3" is discouraged (17 steps).
 Proof modification of "intidOLD" is discouraged (57 steps).
-Proof modification of "intprOLD" is discouraged (112 steps).
-Proof modification of "intprgOLD" is discouraged (80 steps).
 Proof modification of "inxpOLD" is discouraged (115 steps).
 Proof modification of "iotaexOLD" is discouraged (57 steps).
 Proof modification of "iotassuniOLD" is discouraged (35 steps).
@@ -21284,7 +21258,6 @@ Proof modification of "nelbOLD" is discouraged (46 steps).
 Proof modification of "nfa1-o" is discouraged (8 steps).
 Proof modification of "nfaba1OLD" is discouraged (9 steps).
 Proof modification of "nfabdwOLD" is discouraged (152 steps).
-Proof modification of "nfceqdfOLD" is discouraged (48 steps).
 Proof modification of "nfcrALT" is discouraged (20 steps).
 Proof modification of "nfdifOLD" is discouraged (31 steps).
 Proof modification of "nfequid-o" is discouraged (8 steps).
@@ -21437,7 +21410,6 @@ Proof modification of "predasetexOLD" is discouraged (16 steps).
 Proof modification of "predonOLD" is discouraged (29 steps).
 Proof modification of "preleqALT" is discouraged (115 steps).
 Proof modification of "prfiALT" is discouraged (30 steps).
-Proof modification of "prmdvdssqOLD" is discouraged (62 steps).
 Proof modification of "prmgaplcm" is discouraged (247 steps).
 Proof modification of "prmgapprmo" is discouraged (387 steps).
 Proof modification of "problem1" is discouraged (20 steps).
@@ -21480,7 +21452,6 @@ Proof modification of "rabeqcOLD" is discouraged (37 steps).
 Proof modification of "rabexgOLD" is discouraged (21 steps).
 Proof modification of "rabid2OLD" is discouraged (57 steps).
 Proof modification of "rabrabiOLD" is discouraged (38 steps).
-Proof modification of "ral0OLD" is discouraged (12 steps).
 Proof modification of "ralabOLD" is discouraged (40 steps).
 Proof modification of "ralbidaOLD" is discouraged (43 steps).
 Proof modification of "ralcom13OLD" is discouraged (58 steps).
@@ -21489,8 +21460,6 @@ Proof modification of "ralcom4OLD" is discouraged (63 steps).
 Proof modification of "raleleqOLD" is discouraged (26 steps).
 Proof modification of "raleqOLD" is discouraged (11 steps).
 Proof modification of "raleqbidvvOLD" is discouraged (98 steps).
-Proof modification of "ralf0OLD" is discouraged (41 steps).
-Proof modification of "ralidmOLD" is discouraged (68 steps).
 Proof modification of "ralimaOLD" is discouraged (68 steps).
 Proof modification of "ralprgOLD" is discouraged (17 steps).
 Proof modification of "ralrexbidOLD" is discouraged (65 steps).
@@ -21568,7 +21537,6 @@ Proof modification of "reximiaOLD" is discouraged (21 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 "rexn0OLD" is discouraged (17 steps).
 Proof modification of "rexprgOLD" is discouraged (17 steps).
 Proof modification of "rexsngOLD" is discouraged (10 steps).
 Proof modification of "rexxfr3dALT" is discouraged (133 steps).
@@ -21810,8 +21778,6 @@ Proof modification of "undomOLD" is discouraged (322 steps).
 Proof modification of "unexOLD" is discouraged (19 steps).
 Proof modification of "unexbOLD" is discouraged (92 steps).
 Proof modification of "unexgOLD" is discouraged (32 steps).
-Proof modification of "uniprOLD" is discouraged (134 steps).
-Proof modification of "uniprgOLD" is discouraged (80 steps).
 Proof modification of "unipwr" is discouraged (32 steps).
 Proof modification of "unipwrVD" is discouraged (41 steps).
 Proof modification of "unisnALT" is discouraged (146 steps).
@@ -21868,7 +21834,6 @@ Proof modification of "vd03" is discouraged (19 steps).
 Proof modification of "vd12" is discouraged (12 steps).
 Proof modification of "vd13" is discouraged (18 steps).
 Proof modification of "vd23" is discouraged (15 steps).
-Proof modification of "vexOLD" is discouraged (17 steps).
 Proof modification of "vfermltlALT" is discouraged (279 steps).
 Proof modification of "vk15.4j" is discouraged (217 steps).
 Proof modification of "vk15.4jVD" is discouraged (268 steps).
@@ -21879,7 +21844,6 @@ Proof modification of "vtocl3gaOLDOLD" is discouraged (45 steps).
 Proof modification of "vtocl3gafOLD" is discouraged (185 steps).
 Proof modification of "vtocl4gaOLD" is discouraged (166 steps).
 Proof modification of "vtoclOLD" is discouraged (17 steps).
-Proof modification of "vtocldOLD" is discouraged (21 steps).
 Proof modification of "vtocleOLD" is discouraged (12 steps).
 Proof modification of "vtoclegftOLD" is discouraged (50 steps).
 Proof modification of "vtoclfOLD" is discouraged (28 steps).