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;

added termination of narrowing

really need 64bit here; prefer explicit version information for contrib;

Added termination proof for widening

switch afp test to Darwin on macbroy2

merged

introduced commands over a set of vars

basic support for PIDE Scala programming, independently of the main Isabelle repository;

fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick

updated message