src/HOL/Probability/Projective_Limit.thy
changeset 59771 c6e60787ffe2
parent 58876 1888e3cb8048
child 60585 48fdff264eb2