more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
theory Probabilityimports Discrete_Topology Complete_Measure Probability_Measure Infinite_Product_Measure Projective_Limit Independent_Family Information Distributionsbeginend