perm filename EKL[3,2]3 blob sn#625180 filedate 1981-11-22 generic text, type T, neo UTF8
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].
(Note: this manual is currently not up to date.)
For less complete online documentation, see EKL.MAN[EKL,JK].

The manual for the old version of EKL (which is still in use at LOTS)

EKL has recently (November 1981) undergone rather major changes.  To
use the version which existed before November 20, 1981, say

	.run okl[ekl,jk]

to the monitor.  To get functions which simulate TAUT, DEC, etc. (which
no longer exist), give EKL the command

	(fasload (dsk (ekl jk)) fix fas)

or include such a line in your EKL.INI file.