src/HOL/Probability/Bochner_Integration.thy
changeset 59771 c6e60787ffe2
parent 59587 8ea7b22525cb
child 59867 58043346ca64