--- a/src/HOL/Transcendental.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Transcendental.thy Wed Apr 02 18:35:07 2014 +0200
@@ -994,7 +994,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
unfolding continuous_def by (rule tendsto_exp)
-lemma continuous_on_exp [continuous_on_intros]:
+lemma continuous_on_exp [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
unfolding continuous_on_def by (auto intro: tendsto_exp)
@@ -1303,7 +1303,7 @@
"continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
unfolding continuous_within by (rule tendsto_ln)
-lemma continuous_on_ln [continuous_on_intros]:
+lemma continuous_on_ln [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
unfolding continuous_on_def by (auto intro: tendsto_ln)
@@ -1747,7 +1747,7 @@
shows "isCont (\<lambda>x. log (f x) (g x)) a"
using assms unfolding continuous_at by (rule tendsto_log)
-lemma continuous_on_log[continuous_on_intros]:
+lemma continuous_on_log[continuous_intros]:
assumes "continuous_on s f" "continuous_on s g"
and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
shows "continuous_on s (\<lambda>x. log (f x) (g x))"
@@ -2076,7 +2076,7 @@
shows "isCont (\<lambda>x. (f x) powr g x) a"
using assms unfolding continuous_at by (rule tendsto_powr)
-lemma continuous_on_powr[continuous_on_intros]:
+lemma continuous_on_powr[continuous_intros]:
assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
@@ -2215,7 +2215,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
unfolding continuous_def by (rule tendsto_sin)
-lemma continuous_on_sin [continuous_on_intros]:
+lemma continuous_on_sin [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
unfolding continuous_on_def by (auto intro: tendsto_sin)
@@ -2223,7 +2223,7 @@
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
unfolding continuous_def by (rule tendsto_cos)
-lemma continuous_on_cos [continuous_on_intros]:
+lemma continuous_on_cos [continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
unfolding continuous_on_def by (auto intro: tendsto_cos)
@@ -2884,7 +2884,7 @@
"continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
unfolding continuous_within by (rule tendsto_tan)
-lemma continuous_on_tan [continuous_on_intros]:
+lemma continuous_on_tan [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
unfolding continuous_on_def by (auto intro: tendsto_tan)
@@ -3232,7 +3232,7 @@
lemma continuous_on_arcsin': "continuous_on {-1 .. 1} arcsin"
proof -
have "continuous_on (sin ` {- pi / 2 .. pi / 2}) arcsin"
- by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arcsin_sin)
+ by (rule continuous_on_inv) (auto intro: continuous_intros simp: arcsin_sin)
also have "sin ` {- pi / 2 .. pi / 2} = {-1 .. 1}"
proof safe
fix x :: real
@@ -3244,7 +3244,7 @@
finally show ?thesis .
qed
-lemma continuous_on_arcsin [continuous_on_intros]:
+lemma continuous_on_arcsin [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arcsin (f x))"
using continuous_on_compose[of s f, OF _ continuous_on_subset[OF continuous_on_arcsin']]
by (auto simp: comp_def subset_eq)
@@ -3256,7 +3256,7 @@
lemma continuous_on_arccos': "continuous_on {-1 .. 1} arccos"
proof -
have "continuous_on (cos ` {0 .. pi}) arccos"
- by (rule continuous_on_inv) (auto intro: continuous_on_intros simp: arccos_cos)
+ by (rule continuous_on_inv) (auto intro: continuous_intros simp: arccos_cos)
also have "cos ` {0 .. pi} = {-1 .. 1}"
proof safe
fix x :: real
@@ -3268,7 +3268,7 @@
finally show ?thesis .
qed
-lemma continuous_on_arccos [continuous_on_intros]:
+lemma continuous_on_arccos [continuous_intros]:
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. -1 \<le> f x \<and> f x \<le> 1) \<Longrightarrow> continuous_on s (\<lambda>x. arccos (f x))"
using continuous_on_compose[of s f, OF _ continuous_on_subset[OF continuous_on_arccos']]
by (auto simp: comp_def subset_eq)
@@ -3292,7 +3292,7 @@
lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
unfolding continuous_def by (rule tendsto_arctan)
-lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
+lemma continuous_on_arctan [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
unfolding continuous_on_def by (auto intro: tendsto_arctan)
lemma DERIV_arcsin: