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;