Add // as an lcsymtacs alias for THEN; fix hol-mode bug in handling of THEN1
New simplification variants in lcsymtacs (w/CONJ_ss and DNF_ss)
Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.)  Still need to
implement change to EmitTeX.