envirn部のマージ

NAT_1とO_RING_1のマージ例。そのまま2つをコピペしてもエラー。

次のようにディレクティブごとに揃える。

environ

:: From NAT_1, O_RING_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
 vocabularies NAT_1, XBOOLE_0, ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4, RELAT_1,
      ARYTM_3, PARTFUN1, XXREAL_0, CARD_1, FUNCT_1, SQUARE_1, O_RING_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
 notations ORDINAL1, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, NUMBERS,
      STRUCT_0, ALGSTR_0, VECTSP_1, XXREAL_0;

 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;
 constructors RLVECT_1, PARTFUN1, XXREAL_0, NAT_1, VECTSP_1, RELSET_1, GROUP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;
 registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, NAT_1;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 requirements NUMERALS, SUBSET, ARITHM, BOOLE;

EmacsのC-c C-cとC-x `により、重複部分をコメントアウト。とりあえず、vocabulariesに関してやる。

environ

:: From NAT_1, O_RING_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
 vocabularies
      :: NAT_1, XBOOLE_0,
      ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4,
      :: RELAT_1,
      :: ARYTM_3,
      :: PARTFUN1,
      :: XXREAL_0,
      :: CARD_1,
      :: FUNCT_1,
      SQUARE_1, O_RING_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
 :: notations ORDINAL1, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, NUMBERS,
 ::      STRUCT_0, ALGSTR_0, VECTSP_1, XXREAL_0;

 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;
:: constructors RLVECT_1, PARTFUN1, XXREAL_0, NAT_1, VECTSP_1, RELSET_1, GROUP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;
:: registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, NAT_1;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
:: requirements NUMERALS, SUBSET, ARITHM, BOOLE;

作業途中で、

• *830: Nothing imported from notations

となったりする。notationsとvocabulariesでの同じアーティクルの出現が重複になったりするようだ。

environ

:: From NAT_1, O_RING_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
 vocabularies
      :: NAT_1, XBOOLE_0,
      ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4,
      :: RELAT_1,
      :: ARYTM_3,
      :: PARTFUN1,
      :: XXREAL_0,
      :: CARD_1,
      :: FUNCT_1,
      SQUARE_1, O_RING_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
:: notations 
      :: ORDINAL1,
      :: XCMPLX_0, NAT_1, FUNCT_1,
      :: FINSEQ_1, (nothing, already voc)
      :: PARTFUN1, NUMBERS,
      :: STRUCT_0; (nothing, already voc)
      :: ALGSTR_0, VECTSP_1; (nothing, already voc)
      :: XXREAL_0;


 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;
 constructors RLVECT_1,
       :: PARTFUN1, XXREAL_0, NAT_1,
       VECTSP_1,
       :: RELSET_1,
       GROUP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;
 registrations
      :: RELSET_1, XREAL_0,
      STRUCT_0, VECTSP_1,
      :: ORDINAL1,
      NAT_1;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
:: requirements NUMERALS, SUBSET, ARITHM, BOOLE;