hoelzl [Wed, 07 Dec 2011 15:10:29 +0100] rev 45777
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space