diff -r 21e9bd6cf0a8 -r 5c714fd55b1e src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Sep 02 19:57:16 2010 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Thu Sep 02 20:29:12 2010 +0200
@@ -26,14 +26,13 @@
   let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)"
 
   show "finite_measure_space M \<mu>"
-  proof (rule finite_Pow_additivity_sufficient, simp_all)
-    show "positive \<mu>" by (simp add: positive_def)
-
-    show "additive M \<mu>"
-      by (simp add: additive_def inverse_eq_divide field_simps Real_real
+  proof (rule finite_measure_spaceI)
+    fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M"
+    then show "\<mu> (A \<union> B) = \<mu> A + \<mu> B"
+      by (simp add: inverse_eq_divide field_simps Real_real
                     divide_le_0_iff zero_le_divide_iff
                     card_Un_disjoint finite_subset[OF _ finite])
-  qed
+  qed auto
 qed simp_all
 
 lemma set_of_list_extend: