src/HOL/Analysis/measurable.ML
changeset 83239 0da2f7981483
parent 81954 6f2bcdfa9a19