Re: [mizar] Why I cannot quote a theorem

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

On Sat, 29 Nov 2003, Piotr Rudnicki wrote:

> In the text below I am unable to quote a theorem. Why?

>  notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ARYTM_0, XCMPLX_0,
>       XREAL_0, ZFMISC_1, REAL_1, SQUARE_1, INT_1, INT_2, NAT_1, ABSVALUE,
>       POWER, RLVECT_1, CARD_3, VECTSP_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1,
>       FUNCT_2, FINSEQ_1, RAT_1, FINSEQ_2, FINSEQ_4, FINSOP_1, PARTFUN1,
>       TOPREAL1, COMPLEX1, NORMSP_1, BINARITH, RVSUM_1, FVSUM_1, ALGSEQ_1,
>       COMPLFLD, HAHNBAN1, POLYNOM3, POLYNOM4, POLYNOM5, COMPTRIG,
>       CARD_1, COMPLSP1, GROUP_2, SIN_COS, PREPOWER, FINSET_1, GROUP_1,
>       WELLFND1, MCART_1, PRE_CIRC, MOD_2, ENUMSET1, GRAPH_2, FUNCT_4, ORDINAL1,
>       RLVECT_2, CQC_LANG, GROUP_6, DTCONSTR, RFINSEQ, PRALG_1, POLYNOM1,
>       WSIERP_1, PBOOLE, SEQM_3, MEMBERED;

In this environment the FVSUM_1 notation is overloaded by
POLYNOM1.

Greetings from Edinburgh,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================