src/HOL/Probability/Caratheodory.thy
changeset 46731 5302e932d1e5
parent 44928 7ef6505bde7f
child 47694 05663f75964c
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 20:20:09 2012 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 21:53:36 2012 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4      by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
     1.5    moreover
     1.6    have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
     1.7 -    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
     1.8 +    by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
     1.9    ultimately show ?thesis
    1.10      by (metis lambda_system_Compl lambda_system_Int xl yl)
    1.11  qed
    1.12 @@ -666,7 +666,7 @@
    1.13                    (\<lambda>x. Inf (measure_set M f x))"
    1.14  proof (simp add: countably_subadditive_def, safe)
    1.15    fix A :: "nat \<Rightarrow> 'a set"
    1.16 -  let "?outer B" = "Inf (measure_set M f B)"
    1.17 +  let ?outer = "\<lambda>B. Inf (measure_set M f B)"
    1.18    assume A: "range A \<subseteq> Pow (space M)"
    1.19       and disj: "disjoint_family A"
    1.20       and sb: "(\<Union>i. A i) \<subseteq> space M"