src/HOL/Probability/Characteristic_Functions.thy
changeset 69987 e7648f104d6b
parent 67977 557ea2740125
child 70097 4005298550a6