EKL is a programmable interactive proof checker and constructor. It is written in MACLISP. You can spool yourself a manual by typing DOVER EKLMAN.PRE[EKL,JJW]. For less complete online documentation, see EKL.MAN[EKL,JK]. The manual for the old version of EKL (which is still in use at SCORE and LOTS) is on EKLOLD.PRE[EKL,JJW].