recover implicit thread position for status messages (cf. eca8acb42e4a);

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;

re-generated SMT certificates

new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code

ghost bullet via markup, which is painted as bar under text (normally space);

replace induction by hammer

merged

merged;

basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);

maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;

tuned;

proper default browser info for interactive mode, notably thy_deps;

improved pretty printing for state set acom

Improvements to the print_dependencies command.

discontinued obsolete parallel_proofs_reuse_timing;

merged

separate isatest with skip_proofs, to give some impression of performance without most of the proofs;

merged

extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;