A summary of the contents of the subdirectory misc/emacs/ under
Pc-Nqthm-1992:

checkpoints.el, checkpoint-keys.el:  implementations of the feature
described in Computational Logic Technical Report 85, for assisting
users when browsing Nqthm output.

nqthm-compare-windows.el:  a modification of compare-windows that can
be used to compare nqthm proof outputs.  Unlike compare-windows, the
function nqthm-compare-windows ignores differences in Nqthm time
triples.  The algorithm is that when compare-windows gets ``stuck,''
it looks to see if the first character on each window's line is a left
square bracket, and if so then it moves the cursor down a line in each
window and does compare-windows again, etc.