clarified;

replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace

merged

clarified output;

more tooltips;

clarified imports;

update strictly local imports only;

proper imports_base;

tuned;

avoid redundant Preview documents;

HOL-Probability: add measurable space for trees

clarified import of loaded theory;