environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, SUBSET_1, FINSEQ_1, GOBOARD1, XXREAL_0, PARTFUN1, RELAT_1, INCSP_1, MATRIX_1, TREES_1, XBOOLE_0, CARD_1, ARYTM_3, NAT_1, TARSKI, FUNCT_1, ARYTM_1, ZFMISC_1, COMPLEX1, ORDINAL4, TOPREAL1, REAL_1, XXREAL_1, GOBOARD2, MCART_1, TOPREAL4, GOBOARD4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, TOPREAL4, GOBOARD1, GOBOARD2;
definitions TARSKI;
theorems TARSKI, NAT_1, ZFMISC_1, FINSEQ_1, ABSVALUE, FINSEQ_2, TOPREAL1, TOPREAL4, GOBOARD1, GOBOARD2, FINSEQ_3, FINSEQ_4, FUNCT_1, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_1, PARTFUN1, SEQM_3, SEQ_4, MATRIX_0;
schemes NAT_1, FINSEQ_4;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, VALUED_0, CARD_1, GOBOARD1, NAT_1, INT_1;
constructors HIDDEN, XXREAL_1, COMPLEX1, FINSEQ_3, TOPREAL1, TOPREAL4, GOBOARD2, GOBOARD1, RELSET_1, REAL_1, MATRIX_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;