src/HOL/Probability/Bochner_Integration.thy
changeset 59842 9fda99b3d5ee
parent 59587 8ea7b22525cb
child 59867 58043346ca64
equal deleted inserted replaced
59841:2551ac44150e 59842:9fda99b3d5ee