additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);

updated comment to 46b90bbc370d;

recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);

tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);

tuned output -- less bullets;

default implementation of multisets by list with reasonable coverage of operations on multisets

optionalized very specific code setup for multisets

generalized lemma fold_image thanks to Peter Lammich

tuned;

NEWS for 635562bc14ef;

more centralized command timing; clarified old-style timing message;

got rid of legacy smartness

added lemma

merged

amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;

more formal cong_name;

timing status for forked diagnostic commands;

tooltip of command keyword includes timing information;

more operations on Time, Timing;

reverted slip introduced in f738e6dbd844

added 'print_defn_rules' command; tuned;

more item markup; tuned signature;

item markup for Proof_Context.pretty_fact; tuned signature;

obsolete, cf. Proof_Context.print_syntax;

paint bullet bar within text layer -- thus it remains visible with active selection etc.;

Pretty.item markup for improved readability of lists of items;

tuned message;

convenience check for vain instantiation

improved centering via strikethrough offset;