src/HOL/Probability/Characteristic_Functions.thy
changeset 81869 24ef42cab7d6
parent 79599 2c18ac57e92e