src/HOL/Random_Pred.thy
changeset 75458 4117491aa7fe
parent 67091 1393c2340eec
equal deleted inserted replaced
75456:160c9c18a707 75458:4117491aa7fe