src/HOL/Probability/Regularity.thy
changeset 62533 bc25f3916a99
parent 62343 24106dc44def
child 62975 1d066f6ab25d
     1.1 --- a/src/HOL/Probability/Regularity.thy	Mon Mar 07 08:14:18 2016 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Mon Mar 07 14:34:45 2016 +0000
     1.3 @@ -249,7 +249,7 @@
     1.4          fix d
     1.5          have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
     1.6          also have "open \<dots>"
     1.7 -          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
     1.8 +          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)
     1.9          finally have "open (?G d)" .
    1.10        } note open_G = this
    1.11        from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]