This is the README file for the misc/ subdirectory of Pc-Nqthm-1992.
This directory contains various Nqthm-1992 enhancements and relevant
tools that may be of use to Nqthm-1992 users (and hence to
Pc-Nqthm-1992 users as well).  One may load any number of the ".lisp"
files in this directory, though in some cases it is useful to compile
them first and load the compiled files.  Each such file corresponds to
a ".doc" file that documents the utilities to be found there.  None of
these files is necessary for the operation of the Pc-Nqthm-1992
system; in fact they are really not part of that system, but have been
included as part of that system's release for administrative reasons.

This directory is the only part of Pc-Nqthm-1992 that could change
without notice from time to time.  If you have additional
contributions that you'd be willing to include here, please send
electronic mail to kaufmann@cli.com explaining what you have, and I'll
consider including them.  Thank you.

Here is a very brief description of the .lisp files in this directory
at the time of the release.  The subdirectories c/, demos/, and emacs/
have their own README files.

bm-trace.lisp		for tracing Nqthm functions inside R-LOOP
checkpoints.lisp	to assist in the navigation of the prover's
			output in an Emacs environment.
constructive-quantifiers.lisp
			recognizer for quantified notions in Nqthm,
			along with support for generating constructively-
			presented functions that represent quantified notions
identity-speedup.lisp	speeds handling of IDENTITY by about a factor of 2
mutual.lisp		supports mutually recursive definitions
nqthm-setq.lisp		supports assignment for R-LOOP in arbitrary Lisp code
ppte.lisp		prints out "tight" events by generating explicit hints
process-events.lisp	miscellaneous event-processing utilities
purify.lisp		generates event file from database (.lib) file
queries.lisp		miscellaneous Nqthm database query utilities
translate-reader.lisp	assists the user in providing quoted terms for EVAL$
untranslate-with-abbs.lisp
			for introducing abbreviations into Nqthm output

-- Matt Kaufmann