diff -r f51985ebd152 -r 19b7ace1c5da src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Fri Jun 13 07:05:01 2014 +0200 +++ b/src/HOL/Probability/Probability.thy Fri Jun 13 14:08:20 2014 +0200 @@ -6,7 +6,6 @@ Infinite_Product_Measure Projective_Limit Independent_Family - Information Distributions begin