just one data slot per program unit; tuned signature;

more standard configuration options;

tuned;

just one data slot per program unit;

tuned;

more frugal Local_Syntax.init -- maintain idents within context;

proper exception for internal program failure, not user-error;

tuned;

suppress irrelevant timing messages (the majority);

less ambitious settings -- increase chances of success;

peek value without synchronization;

avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;

tuning

unfortunately, there is no general function space in the measurable spaces

correctly apply type substitution before checking for function types

avoid generating selectors with function types -- this produce arity inconsistencies

renamed theory file

merged

Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);

tuned;

tuned;

added Par_List in Scala, in accordance to ML version; system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML; avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation; tuned;

tuned;

rel_pmf commutes with rel_prod

note more facts (always)

conceal typedef more violently

respect order of deads when retrieving bnfs from the database

merged

more informative gutter content: fall-back on background color, e.g. when line numbers are enabled; non-transparent information_message_color like other message colors; removed unused error1_color;

more examples;