8.1.2 Checking the Environ Section

In addition, we have to check the environ section. To do this, there are the following commands.


      IRRVOC     Checks unnecessary vocabulary.
      IRRTHS     Checks unnecessary theorems.


    The method of using these is the same with the checking commands of the main section. For NOTATION and CONSTRUSTORS, there is no good way of checking. Therefore, use NOTATION and CONSTRUSTORS sparingly from the beginning and start with 0 and gradually include what is needed. However, if we accommodate after deleting an unnecessary file by IRRVOC, an error will appear in the NOTATION section, so we will be able to remove it.