Keyword 'rewrites' identifies rewrite morphisms.

Qualifiers in locale expressions default to mandatory regardless of the command.

merged

tuned signature;

prefer Isabelle/Scala Future;

prefer Isabelle/Scala Future;

tuned imports;

more direct task future implementation, with proper cancel operation; more uniform Future.thread;

tuned;

prefer ad-hoc non-worker threads;

clarified modules;

cancel already running request;

added acknowledgement in Binomial.thy

Merged

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

don't pollute local theory with needless names

allow selectors and discriminators with same name as type

make sure that function types are never generated as '> @ A @ B', but always as 'A > B'

merged

avoid premature flushing and thus flashing of text area;

tuned whitespace;

clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);

redundant;

tuned whitespace;

tuned document;

tuned document;

tuned document;

isabelle update_cartouches -t;

avoid highlighted area getting "stuck" after edit;

clarified completion of Isabelle symbols within document source;