Open
Description
I wanted to search a long list of theorems but it didn't work. Probably because it's too long.
MM-PA> search
What are the labels to match (* = wildcard) <*>?dfacacn,dfac12lem1,infmap2,ackbij2lem2,ackbij2lem3,fin23lem32,konigthlem,wunex2,wuncval2,rpnnen1lem1,rpnnen1lem3,rpnnen1lem5,mptnn0fsupp,ccatfn,ccatfval,swrdval,swrd00,swrd0,revval,repsundef,climmpt,climle,iserabs,isumshft,divcnvshft,supcvg,trireciplem,expcnv,explecnv,geolim,geo2lim,cvgrat,mertenslem2,eftlub,rpnnen2lem1,rpnnen2lem2,1arithlem1,1arith,vdwapval,vdwlem6,vdwlem9,restfn,cidffn,idfu2nd,idfu1st,idfucl,fucco,homafval,prf1,prf2fval,prfcl,prf1st,prf2nd,curf1fval,curf11,curf12,curf1cl,curf2,curfcl,hof2val,yonedalem3a,yonedalem4a,yonedalem4b,yonedalem4c,yonedalem3,yonedainv,lubfval,glbfval,smndex1gbas,smndex1gid,smndex1igid,smndex1mnd,smndex1id,smndex1n0mnd,smndex2dbas,smndex2hbas,cntzfval,psgnfval,sylow1lem2,sylow2blem1,sylow2blem2,sylow3lem1,sylow3lem6,pj1fval,vrgpfval,lspfval,sraval,zrhval2,aspval,psrmulfval,psrass1,mvrval,mplmon,mplcoe1,evlslem2,mpfrcl,evlsval,evlsvar,mpfind,mhpfval,coe1fval,psropprmul,coe1mul2,ply1coe,evls1fval,evls1val,evl1fval,evl1val,submafval,mdetfval,madufval,minmar1fval,pmatcollpw2lem,pm2mpval,1stcfb,ptbasfi,dfac14,fmval,fmf,flffval,fcfval,cnextval,met1stc,pcoval,iscmet3lem3,rrxsca,mbflimsup,mbflim,itg1climres,mbfi1fseqlem2,mbfi1fseqlem4,mbfi1fseqlem6,mbfi1flimlem,mbfmullem2,itg2monolem1,itg2addlem,itg2cnlem1,cpnfval,mdegfval,elply,plyeq0lem,plypf1,geolim3,ulmuni,ulmcau,ulmdvlem1,ulmdvlem3,mbfulm,itgulm,pserval,dvradcnv,pserdvlem2,abelthlem1,abelthlem3,abelthlem6,logtayl,leibpi,dfef2,emcllem4,emcllem6,emcllem7,lgamgulmlem5,lgamgulmlem6,lgamcvg2,basellem6,sqff1o,dchrptlem2,dchrptlem3,2lgslem1,dchrisumlem3,padicfval,padicabvf,istrkg2ld,mirval,ishpg,lmif,islmib,axlowdim,crctcshlem3,nmoofval,pjhfval,pjmfn,hosmval,hommval,hodmval,hfsmval,hfmmval,eigvalfval,brafval,kbfval,rnbra,bra11,padct,fpwrelmap,qusima,nsgmgc,nsgqusf1o,idlsrgtset,locfinreflem,rspectopn,zarcmplem,ordtconnlem1,xrhval,sigapildsys,sxbrsigalem2,eulerpart,dstfrvclim1,ballotlemfval,ballotlemsval,signstfv,vtsval,cvmliftlem5,mrsubffval,mrsubfval,msubffval,msubfval,msubrn,msubco,msubvrs,circum,divcnvlin,climlec3,faclimlem2,faclim2,knoppcnlem1,knoppcnlem6,knoppcnlem7,cnndvlem2
***BUG #1525
Search for what math symbol string? / or nothing <nothing>? Fin
^^^
?Expected / or nothing.
copyable list:
dfacacn,dfac12lem1,infmap2,ackbij2lem2,ackbij2lem3,fin23lem32,konigthlem,wunex2,wuncval2,rpnnen1lem1,rpnnen1lem3,rpnnen1lem5,mptnn0fsupp,ccatfn,ccatfval,swrdval,swrd00,swrd0,revval,repsundef,climmpt,climle,iserabs,isumshft,divcnvshft,supcvg,trireciplem,expcnv,explecnv,geolim,geo2lim,cvgrat,mertenslem2,eftlub,rpnnen2lem1,rpnnen2lem2,1arithlem1,1arith,vdwapval,vdwlem6,vdwlem9,restfn,cidffn,idfu2nd,idfu1st,idfucl,fucco,homafval,prf1,prf2fval,prfcl,prf1st,prf2nd,curf1fval,curf11,curf12,curf1cl,curf2,curfcl,hof2val,yonedalem3a,yonedalem4a,yonedalem4b,yonedalem4c,yonedalem3,yonedainv,lubfval,glbfval,smndex1gbas,smndex1gid,smndex1igid,smndex1mnd,smndex1id,smndex1n0mnd,smndex2dbas,smndex2hbas,cntzfval,psgnfval,sylow1lem2,sylow2blem1,sylow2blem2,sylow3lem1,sylow3lem6,pj1fval,vrgpfval,lspfval,sraval,zrhval2,aspval,psrmulfval,psrass1,mvrval,mplmon,mplcoe1,evlslem2,mpfrcl,evlsval,evlsvar,mpfind,mhpfval,coe1fval,psropprmul,coe1mul2,ply1coe,evls1fval,evls1val,evl1fval,evl1val,submafval,mdetfval,madufval,minmar1fval,pmatcollpw2lem,pm2mpval,1stcfb,ptbasfi,dfac14,fmval,fmf,flffval,fcfval,cnextval,met1stc,pcoval,iscmet3lem3,rrxsca,mbflimsup,mbflim,itg1climres,mbfi1fseqlem2,mbfi1fseqlem4,mbfi1fseqlem6,mbfi1flimlem,mbfmullem2,itg2monolem1,itg2addlem,itg2cnlem1,cpnfval,mdegfval,elply,plyeq0lem,plypf1,geolim3,ulmuni,ulmcau,ulmdvlem1,ulmdvlem3,mbfulm,itgulm,pserval,dvradcnv,pserdvlem2,abelthlem1,abelthlem3,abelthlem6,logtayl,leibpi,dfef2,emcllem4,emcllem6,emcllem7,lgamgulmlem5,lgamgulmlem6,lgamcvg2,basellem6,sqff1o,dchrptlem2,dchrptlem3,2lgslem1,dchrisumlem3,padicfval,padicabvf,istrkg2ld,mirval,ishpg,lmif,islmib,axlowdim,crctcshlem3,nmoofval,pjhfval,pjmfn,hosmval,hommval,hodmval,hfsmval,hfmmval,eigvalfval,brafval,kbfval,rnbra,bra11,padct,fpwrelmap,qusima,nsgmgc,nsgqusf1o,idlsrgtset,locfinreflem,rspectopn,zarcmplem,ordtconnlem1,xrhval,sigapildsys,sxbrsigalem2,eulerpart,dstfrvclim1,ballotlemfval,ballotlemsval,signstfv,vtsval,cvmliftlem5,mrsubffval,mrsubfval,msubffval,msubfval,msubrn,msubco,msubvrs,circum,divcnvlin,climlec3,faclimlem2,faclim2,knoppcnlem1,knoppcnlem6,knoppcnlem7,cnndvlem2
Metadata
Metadata
Assignees
Labels
No labels