changeset 61169 | 4de9ff3ea29a |
parent 60585 | 48fdff264eb2 |
child 61605 | 1bf7b186542e |
child 61609 | 77b453bd616f |
--- a/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 13 22:56:52 2015 +0200 @@ -993,7 +993,7 @@ note A_in_sets = this show "sigma_finite_measure ?N" - proof (default, intro exI conjI ballI) + proof (standard, intro exI conjI ballI) show "countable (range (\<lambda>(i, j). A i \<inter> Q j))" by auto show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"