TEX-ALL-WFFS : LIBRARYCMDTEX-ALL-WFFS is a library command.
Write all wffs in all files in DEFAULT-LIB-DIR (and optionally BACKUP-LIB-DIR)
to a TeX file.
The three verbosity settings are: MIN, which just shows the names of the
objects, MED, which shows the help messages, provability and wffs as well, and MAX,
which shows everything.
As a filter, you can select any known keywords; only the wffs which
satisfy all of the given keywords will be shown. See SHOW-KEYWORDS
for a list of keywords.
The command format for TEX-ALL-WFFS is:
<LIB>TEX-ALL-WFFS BACKUP FILTER FNAME VERBOSITY
"YESNO" "GWFF-PROP-LIST" "FILESPEC" "SYMBOL"
TPS documentation homepage