src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:02 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 02 18:35:07 2014 +0200
1.3 @@ -791,7 +791,7 @@
1.4  lemma open_ball [intro, simp]: "open (ball x e)"
1.5  proof -
1.6    have "open (dist x -` {..<e})"
1.7 -    by (intro open_vimage open_lessThan continuous_on_intros)
1.8 +    by (intro open_vimage open_lessThan continuous_intros)
1.9    also have "dist x -` {..<e} = ball x e"
1.10      by auto
1.11    finally show ?thesis .
1.12 @@ -2375,7 +2375,7 @@
1.13  lemma closed_cball: "closed (cball x e)"
1.14  proof -
1.15    have "closed (dist x -` {..e})"
1.16 -    by (intro closed_vimage closed_atMost continuous_on_intros)
1.17 +    by (intro closed_vimage closed_atMost continuous_intros)
1.18    also have "dist x -` {..e} = cball x e"
1.19      by auto
1.20    finally show ?thesis .
1.21 @@ -4931,11 +4931,11 @@
1.22
1.23  subsubsection {* Structural rules for setwise continuity *}
1.24
1.25 -lemma continuous_on_infnorm[continuous_on_intros]:
1.26 +lemma continuous_on_infnorm[continuous_intros]:
1.27    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
1.28    unfolding continuous_on by (fast intro: tendsto_infnorm)
1.29
1.30 -lemma continuous_on_inner[continuous_on_intros]:
1.31 +lemma continuous_on_inner[continuous_intros]:
1.32    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
1.33    assumes "continuous_on s f"
1.34      and "continuous_on s g"
1.35 @@ -4945,15 +4945,15 @@
1.36
1.37  subsubsection {* Structural rules for uniform continuity *}
1.38
1.39 -lemma uniformly_continuous_on_id[continuous_on_intros]:
1.40 +lemma uniformly_continuous_on_id[continuous_intros]:
1.41    "uniformly_continuous_on s (\<lambda>x. x)"
1.42    unfolding uniformly_continuous_on_def by auto
1.43
1.44 -lemma uniformly_continuous_on_const[continuous_on_intros]:
1.45 +lemma uniformly_continuous_on_const[continuous_intros]:
1.46    "uniformly_continuous_on s (\<lambda>x. c)"
1.47    unfolding uniformly_continuous_on_def by simp
1.48
1.49 -lemma uniformly_continuous_on_dist[continuous_on_intros]:
1.50 +lemma uniformly_continuous_on_dist[continuous_intros]:
1.51    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
1.52    assumes "uniformly_continuous_on s f"
1.53      and "uniformly_continuous_on s g"
1.54 @@ -4979,20 +4979,20 @@
1.55      unfolding dist_real_def by simp
1.56  qed
1.57
1.58 -lemma uniformly_continuous_on_norm[continuous_on_intros]:
1.59 +lemma uniformly_continuous_on_norm[continuous_intros]:
1.60    assumes "uniformly_continuous_on s f"
1.61    shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
1.62    unfolding norm_conv_dist using assms
1.63    by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
1.64
1.65 -lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]:
1.66 +lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
1.67    assumes "uniformly_continuous_on s g"
1.68    shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
1.69    using assms unfolding uniformly_continuous_on_sequentially
1.70    unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
1.71    by (auto intro: tendsto_zero)
1.72
1.73 -lemma uniformly_continuous_on_cmul[continuous_on_intros]:
1.74 +lemma uniformly_continuous_on_cmul[continuous_intros]:
1.75    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.76    assumes "uniformly_continuous_on s f"
1.77    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
1.78 @@ -5004,12 +5004,12 @@
1.79    shows "dist (- x) (- y) = dist x y"
1.80    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
1.81
1.82 -lemma uniformly_continuous_on_minus[continuous_on_intros]:
1.83 +lemma uniformly_continuous_on_minus[continuous_intros]:
1.84    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.85    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
1.86    unfolding uniformly_continuous_on_def dist_minus .
1.87
1.90    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.91    assumes "uniformly_continuous_on s f"
1.92      and "uniformly_continuous_on s g"
1.93 @@ -5019,7 +5019,7 @@
1.96
1.97 -lemma uniformly_continuous_on_diff[continuous_on_intros]:
1.98 +lemma uniformly_continuous_on_diff[continuous_intros]:
1.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.100    assumes "uniformly_continuous_on s f"
1.101      and "uniformly_continuous_on s g"
1.102 @@ -5031,7 +5031,7 @@
1.103
1.104  lemmas continuous_at_compose = isCont_o
1.105
1.106 -lemma uniformly_continuous_on_compose[continuous_on_intros]:
1.107 +lemma uniformly_continuous_on_compose[continuous_intros]:
1.108    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
1.109    shows "uniformly_continuous_on s (g \<circ> f)"
1.110  proof -
1.111 @@ -6972,7 +6972,7 @@
1.112    apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
1.113    apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
1.114    using assms
1.115 -  apply (auto simp add: continuous_on_intros)
1.116 +  apply (auto simp add: continuous_intros)
1.117    done
1.118
1.119  lemma homeomorphic_translation:
1.120 @@ -7010,14 +7010,14 @@
1.121      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
1.122      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
1.123      using assms
1.124 -    apply (auto intro!: continuous_on_intros
1.125 +    apply (auto intro!: continuous_intros
1.126        simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
1.127      done
1.128    show ?cth unfolding homeomorphic_minimal
1.129      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
1.130      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
1.131      using assms
1.132 -    apply (auto intro!: continuous_on_intros
1.133 +    apply (auto intro!: continuous_intros
1.134        simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
1.135      done
1.136  qed
```