Wed, 07 Dec 2011 15:10:29 +0100 | hoelzl | 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 | changeset | files |
Mon, 05 Dec 2011 15:10:15 +0100 | huffman | remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead | changeset | files |