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;