9.3 To serach for
the ABS file which the terminology appears
9.3.1 Method for Using grep
We may want to know about where the terminology is used in the library. It is the case where there is a question (where to define) or a question (Where and where is the theorem about it). In such a case, although it is not contained in in the standard MIZAR system, it is convenient to use a program called egrep. For example, to list the ABS file in which terminology called Metric appears, we input as foolws.
C:\>/mizar/egrep Metric *.* \| more
An egrep.exe program is free software (by Mr. M.Patnode) and we can get it from the following URL (of the Internet) .
It is convenient if we make it into the batch file including a change of a directory.
In addition, although it may be good to do like the above when searching for the general character string (alphanumeric character), the character string is to be searched for with a regular expression generally. Therefore, in order to search for the file and line which have the sum of three variables like a+b+c or x+y+z, we have to use it as follows.
egrep [a-z]\+[a-z]\+[a-z] *.*
Here, the following means one of the letters from Alphabet a to z, and \+ means the letter of +. And let us keep in mind that we have to write a sign like + or - after backslash \.
Detailed explanation of a regular expression is in large numbers on the Internet. For example, please refer to the next URL.