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;