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;