more exception handling -- make print functions total;

more print function parameters; check command_visible statically in assignment, instead of dynamically in execution;

tuned;

discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;

tuned;

allow multiple print functions;

tuned signature;

tuned signature;

tuned;

tuned signature;

use long goal format in rel_induct theorem

share some code between codatatypes, datatypes and eventually prim(co)rec

tuned names

tuned;

allow choice of target directory (again, see also 58e2d0cd81ae);

postinstall: recover Cygwin permissions;

clarified initial cd;

clarified Proofterm.proofs vs. Goal.skip_proofs;

clarified focus after dismiss;

tuned signature;

avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);

more robust delayed invocation;

clarified tooltip timing of pending event and active state;

less intrusive border, notably on windows;

tighten tooltip size;

visually explicit focus (behaviour dependent on platform and look-and-feel);

tuned;

more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;

discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;

backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;