tuned;

clarified markup: more uniform treatment of parse/print phase;

tuned;

clarified markup: more uniform;

tuned signature: separate markup vs. extern;

clarified signature;

tuned: prefer configuration options via context;

tuned;

tuned signature: more operations;

tuned comments

merged

Partial tidying of old proofs

merged

new version of time_fun that works for classes; define T_length automatically now

merged

revised/generalised some lemmas

remove terminated jobs, even if futures do not complete;

terminate jobs properly;

clarified signature: eliminate clones;

tuned: more antiquotations;

tuned: more antiquotations;

misc tuning;

tuned: eliminate clone (with change of internal exceptions);

tuned: more antiquotations;

tuned comments and whitespace (see also 589645894305);

tuned: more antiquotations;

tuned: more antiquotations;

proper const (see also 759bffe1d416 and b2800da9eb8a);

tuned: inline constants;

tuned: eliminate clone;

tuned: more antiquotations;

prefer host that is less likely to be down;

adapt and activate congprocs examples, following the current Simplifier implementation; minor tuning;

original Congproc_Ex.thy by Norbert Schirmer: still inactive;

provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;

clarified signature;

more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;

tuned;

support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;

tuned;

tuned: anticipate congprocs;

clarified signature;

tuned signature (again): anticipate different kinds of procs;

clarified context data; tuned: more antiquotations;

tuned: prefer canonical argument order;

tuned: more antiquotations;

tuned: prefer canonical argument order;

clarified signature: less redundant types;

clarified signature;

unused (see d12c58e12c51);

tuned signature: support more general procedures;

merged

tuned: more antiquotations;

tuned;

tuned: more antiquotations;

tuned whitespace;

more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;

tuned modules;

misc tuning;

tuned;