more robust connection via proxy_host;

more robust: proper transfer if Context.eq_thy_id;

merged

tuned;

tuned;

more robust hg_url; clarified signature;

proper usage (amending 8c7706b053c7);

proper escape for literal single quotes;

some uses of "' " as witness for this feature;

allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);

tidied up a few little proofs

updated for release;

more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;

tuned for Isabelle2020;

more explicit defaults;

proper transfer for Thm.derivation_name;

tuned OS names;

standard tests for macOS 10.15 Catalina;

updated NEWS w.r.t. e0237f2eb49d

more frugal simp rules for bit operations; more pervasive use of bit selector

more scalable output of YXML files;

proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;

tuned;

tuned whitespace;

more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);

clarified;

tuned signature;

tuned signature;

tuned signature;

tuned;