# HG changeset patch
# User hoelzl
# Date 1362585381 -3600
# Node ID 21e5b6efb317a1937cf8a400084319fc7087f984
# Parent  c4367ed99b5ebee7e51e5d37c708df4867c48c14
changed continuous_intros into a named theorems collection

diff -r c4367ed99b5e -r 21e5b6efb317 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
@@ -4159,95 +4159,102 @@
 
 subsubsection {* Structural rules for pointwise continuity *}
 
-lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
+ML {*
+
+structure Continuous_Intros = Named_Thms
+(
+  val name = @{binding continuous_intros}
+  val description = "Structural introduction rules for pointwise continuity"
+)
+
+*}
+
+setup Continuous_Intros.setup
+
+lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)"
   unfolding continuous_within by (rule tendsto_ident_at_within)
 
-lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)"
+lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)"
   unfolding continuous_at by (rule tendsto_ident_at)
 
-lemma continuous_const: "continuous F (\<lambda>x. c)"
+lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)"
   unfolding continuous_def by (rule tendsto_const)
 
-lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
   unfolding continuous_def by (rule tendsto_fst)
 
-lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
   unfolding continuous_def by (rule tendsto_snd)
 
-lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
   unfolding continuous_def by (rule tendsto_Pair)
 
-lemma continuous_dist:
+lemma continuous_dist[continuous_intros]:
   assumes "continuous F f" and "continuous F g"
   shows "continuous F (\<lambda>x. dist (f x) (g x))"
   using assms unfolding continuous_def by (rule tendsto_dist)
 
-lemma continuous_infdist:
+lemma continuous_infdist[continuous_intros]:
   assumes "continuous F f"
   shows "continuous F (\<lambda>x. infdist (f x) A)"
   using assms unfolding continuous_def by (rule tendsto_infdist)
 
-lemma continuous_norm:
+lemma continuous_norm[continuous_intros]:
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
   unfolding continuous_def by (rule tendsto_norm)
 
-lemma continuous_infnorm:
+lemma continuous_infnorm[continuous_intros]:
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
   unfolding continuous_def by (rule tendsto_infnorm)
 
-lemma continuous_add:
+lemma continuous_add[continuous_intros]:
   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
   unfolding continuous_def by (rule tendsto_add)
 
-lemma continuous_minus:
+lemma continuous_minus[continuous_intros]:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
   unfolding continuous_def by (rule tendsto_minus)
 
-lemma continuous_diff:
+lemma continuous_diff[continuous_intros]:
   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
   unfolding continuous_def by (rule tendsto_diff)
 
-lemma continuous_scaleR:
+lemma continuous_scaleR[continuous_intros]:
   fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
   unfolding continuous_def by (rule tendsto_scaleR)
 
-lemma continuous_mult:
+lemma continuous_mult[continuous_intros]:
   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
   shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
   unfolding continuous_def by (rule tendsto_mult)
 
-lemma continuous_inner:
+lemma continuous_inner[continuous_intros]:
   assumes "continuous F f" and "continuous F g"
   shows "continuous F (\<lambda>x. inner (f x) (g x))"
   using assms unfolding continuous_def by (rule tendsto_inner)
 
-lemma continuous_inverse:
+lemma continuous_inverse[continuous_intros]:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
   shows "continuous F (\<lambda>x. inverse (f x))"
   using assms unfolding continuous_def by (rule tendsto_inverse)
 
-lemma continuous_at_within_inverse:
+lemma continuous_at_within_inverse[continuous_intros]:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
   using assms unfolding continuous_within by (rule tendsto_inverse)
 
-lemma continuous_at_inverse:
+lemma continuous_at_inverse[continuous_intros]:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   assumes "continuous (at a) f" and "f a \<noteq> 0"
   shows "continuous (at a) (\<lambda>x. inverse (f x))"
   using assms unfolding continuous_at by (rule tendsto_inverse)
 
-lemmas continuous_intros = continuous_at_id continuous_within_id
-  continuous_const continuous_dist continuous_norm continuous_infnorm
-  continuous_add continuous_minus continuous_diff continuous_scaleR continuous_mult
-  continuous_inner continuous_at_inverse continuous_at_within_inverse
-
 subsubsection {* Structural rules for setwise continuity *}
 
 lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"