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