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.