updated "Control and search tacticals" (moved from ref to implementation); discontinued odd trace flags that assume sequential TTY loop; discontinued obscure DETERM_UNTIL_SOLVED; discontinued obsolete chapter "Tacticals" (ref);

obsolete -- covered in implementation manual;

moved HEADGOAL; added RANGE;

removed some obscure material; misc tuning;

added SELECT_GOAL;

tuned;

updated "subgoal quantifiers";

tuned ML infixes;

document antiquotations for ML infix operators;

tuned;