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])
```