TEXLIBFILE : LIBRARYCMDTEXLIBFILE is a library command.
Print the specified library files into TeX files.
The three verbosity settings are: MIN, which just shows the names of the
objects, MED, which shows the help messages, keywords, provability and wffs
as well, and MAX, which shows everything. It can take a list of filenames
and a corresponding list of output files; if the latter list is too long it
will be truncated, and if it is too short then the last filename given will
be used for all the remaining output (so you can write a group of library
files to a single output file by only supplying one output filename).
After leaving TPS, run the .tex files through TeX and print the resulting
The command format for TEXLIBFILE is:
<LIB>TEXLIBFILE FILENAMESIN FILENAMESOUT VERBOSITY
"FILESPECLIST" "FILESPECLIST" "SYMBOL"
TPS documentation homepage