----------------------------------------------------------------------

Committing in a modification to developers/releasing-hol that includes
the pred_set library documentation. To make this easier to include
the documentation from several libraries, wrote a script that uses
the library name as the name of the documentation. Moved the
name of the pred_set library documentation from pred_sets.{dvi,ps,pdf}
to pred_set.{dvi,ps,pdf}.

Modified Files:
hol98/developers/releasing-hol
hol98/src/pred_set/Manual/Makefile
hol98/src/pred_set/Manual/index.tex
Added Files:
hol98/src/pred_set/Manual/pred_set.tex
Removed Files:
hol98/src/pred_set/Manual/pred_sets.tex
----------------------------------------------------------------------