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);
use_thys [
"Integration",
"Isar",
"Local_Theory",
"Logic",
"ML",
"Prelim",
"Proof",
"Syntax",
"Tactic"
];