src/HOL/Probability/SPMF.thy
changeset 77820 15edec78869c
parent 77434 da41823d09a7
child 78517 28c1f4f5335f
equal deleted inserted replaced
77819:d2645d3ad9e9 77820:15edec78869c