removed obscure material;

updated rotate_tac;

tuned;

updated citations;

updated subgoal_tac;

tuned sectioning;

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;

updated repetition tacticals; discontinued odd trace_REPEAT (assumes sequential TTY loop);

updated THEN, ORELSE, APPEND, and derivatives; discontinued obscure INTLEAVE;

removed obscure/outdated material;

updated RSN, RL, RLN, MRS; discontinued obscure MRL;

removed obscure/outdated material;

tuned;

more on Logic.all/mk_implies etc.;

reduce AFP test by many hours;