src/HOL/Transcendental.thy
changeset 51481 ef949192e5d6
parent 51478 270b21f3ae0a
child 51482 80efd8c49f52
     1.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -2457,17 +2457,6 @@
     1.4  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
     1.5    using arctan_eq_iff [of x 0] by simp
     1.6  
     1.7 -lemma isCont_inverse_function2: (* generalize with continuous_on *)
     1.8 -  fixes f g :: "real \<Rightarrow> real" shows
     1.9 -  "\<lbrakk>a < x; x < b;
    1.10 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
    1.11 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
    1.12 -   \<Longrightarrow> isCont g (f x)"
    1.13 -apply (rule isCont_inverse_function
    1.14 -       [where f=f and d="min (x - a) (b - x)"])
    1.15 -apply (simp_all add: abs_le_iff)
    1.16 -done
    1.17 -
    1.18  lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
    1.19  apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
    1.20  apply (rule isCont_inverse_function2 [where f=sin])