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;