src/HOL/Probability/Projective_Limit.thy
changeset 60536 00db0d934a7d
parent 58876 1888e3cb8048
child 60585 48fdff264eb2