avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

tuned text

corrected nonsensical associativity of `` and dvd

add exponential and uniform distributions

fundamental theorem of calculus for the Lebesgue integral

add Int_atMost

more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;