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