src/HOL/Multivariate_Analysis/Integration.thy
changeset 41969 1cf3e4107a2a
parent 41958 5abc60a017e0
child 42869 43b0f61f56d0
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 12:34:12 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 14:37:33 2011 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
     1.6  (*  Author:                     John Harrison
     1.7      Translation from HOL light: Robert Himmelmann, TU Muenchen *)
     1.8 @@ -3780,7 +3779,7 @@
     1.9    shows "f x = y"
    1.10  proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
    1.11      apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
    1.12 -    apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing])
    1.13 +    apply(rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
    1.14      apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
    1.15    proof safe fix x assume "x\<in>s" 
    1.16      from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]