modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
theory Probabilityimports Discrete_Topology Complete_Measure Probability_Measure Infinite_Product_Measure Projective_Limit Independent_Family Information Distributionsbeginend