1.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Sep 02 19:57:16 2010 +0200
     1.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Sep 02 20:29:12 2010 +0200
     1.3 @@ -26,14 +26,13 @@
     1.4    let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)"
     1.5  
     1.6    show "finite_measure_space M \<mu>"
     1.7 -  proof (rule finite_Pow_additivity_sufficient, simp_all)
     1.8 -    show "positive \<mu>" by (simp add: positive_def)
     1.9 -
    1.10 -    show "additive M \<mu>"
    1.11 -      by (simp add: additive_def inverse_eq_divide field_simps Real_real
    1.12 +  proof (rule finite_measure_spaceI)
    1.13 +    fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M"
    1.14 +    then show "\<mu> (A \<union> B) = \<mu> A + \<mu> B"
    1.15 +      by (simp add: inverse_eq_divide field_simps Real_real
    1.16                      divide_le_0_iff zero_le_divide_iff
    1.17                      card_Un_disjoint finite_subset[OF _ finite])
    1.18 -  qed
    1.19 +  qed auto
    1.20  qed simp_all
    1.21  
    1.22  lemma set_of_list_extend: