This file contains miscellaneous documentation for Pc-Nqthm-1992.  The
primary documentation for this system is described under the heading
"DOCUMENTATION" in the README-pc file of the top-level Pc-Nqthm-1992
directory.

The file defn-sk.doc described extensions to the functionality of
DEFN-SK that have appeared since the time that the primary
documentation was written.  Briefly, there have been two improvements
to DEFN-SK.  First, both COND and CASE syntax may now be used to build
formulas (not just terms).  Second, one may now give hints that
specify the order of arguments to Skolem functions.  The new DEFN-SK
is intended to be fully upward-compatible with the existing version.
Further details may be found in defn-sk.doc.

The file release-notes.txt contains a history of enhancements to
Pc-Nqthm.  The most recent changes are described in the final section
of that file, entitled ``Release "1992".''
