This is a system of propsositional calculsu used in
Logic, Proof and Computation.  To load it
enter (tc +) to enable type checking and then
(load "<pathname to syntax.shen>") and
(load "<pathname to derivationrules.shen>").