src/HOL/Probability/Bochner_Integration.thy
changeset 63625 1e7c5bbea36d
parent 63566 e5abbdee461a