src/HOL/Probability/Borel_Space.thy
changeset 44928 7ef6505bde7f
parent 44890 22f665a2e91c
child 45287 97df8c08291c
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -1414,7 +1414,7 @@
     1.4  proof
     1.5    fix a
     1.6    have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
     1.7 -    by (auto simp: less_SUP_iff SUPR_apply)
     1.8 +    by (auto simp: less_SUP_iff SUP_apply)
     1.9    then show "?sup -` {a<..} \<inter> space M \<in> sets M"
    1.10      using assms by auto
    1.11  qed
    1.12 @@ -1427,7 +1427,7 @@
    1.13  proof
    1.14    fix a
    1.15    have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
    1.16 -    by (auto simp: INF_less_iff INFI_apply)
    1.17 +    by (auto simp: INF_less_iff INF_apply)
    1.18    then show "?inf -` {..<a} \<inter> space M \<in> sets M"
    1.19      using assms by auto
    1.20  qed