src/HOL/Probability/Projective_Limit.thy
changeset 81913 5b9aca9b073b
parent 80914 d97fdabd9e2b
child 82802 547335b41005