src/HOL/Probability/Bochner_Integration.thy
changeset 63393 c22928719e19
parent 63092 a949b2a5f51d
child 63566 e5abbdee461a