1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 16:48:05 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 18:35:36 2011 -0700
     1.3 @@ -1101,8 +1101,7 @@
     1.4  
     1.5  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
     1.6    unfolding Collect_all_eq
     1.7 -  by (intro closed_INT ballI closed_Collect_le continuous_const
     1.8 -    continuous_at_component)
     1.9 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.10  
    1.11  lemma Lim_component_cart:
    1.12    fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
    1.13 @@ -1289,14 +1288,12 @@
    1.14  lemma closed_interval_left_cart: fixes b::"real^'n"
    1.15    shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
    1.16    unfolding Collect_all_eq
    1.17 -  by (intro closed_INT ballI closed_Collect_le continuous_const
    1.18 -    continuous_at_component)
    1.19 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.20  
    1.21  lemma closed_interval_right_cart: fixes a::"real^'n"
    1.22    shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
    1.23    unfolding Collect_all_eq
    1.24 -  by (intro closed_INT ballI closed_Collect_le continuous_const
    1.25 -    continuous_at_component)
    1.26 +  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    1.27  
    1.28  lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
    1.29    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
    1.30 @@ -1304,19 +1301,19 @@
    1.31  
    1.32  lemma closed_halfspace_component_le_cart:
    1.33    shows "closed {x::real^'n. x$i \<le> a}"
    1.34 -  by (intro closed_Collect_le continuous_at_component continuous_const)
    1.35 +  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    1.36  
    1.37  lemma closed_halfspace_component_ge_cart:
    1.38    shows "closed {x::real^'n. x$i \<ge> a}"
    1.39 -  by (intro closed_Collect_le continuous_at_component continuous_const)
    1.40 +  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    1.41  
    1.42  lemma open_halfspace_component_lt_cart:
    1.43    shows "open {x::real^'n. x$i < a}"
    1.44 -  by (intro open_Collect_less continuous_at_component continuous_const)
    1.45 +  by (intro open_Collect_less vec_nth.isCont isCont_const)
    1.46  
    1.47  lemma open_halfspace_component_gt_cart:
    1.48    shows "open {x::real^'n. x$i  > a}"
    1.49 -  by (intro open_Collect_less continuous_at_component continuous_const)
    1.50 +  by (intro open_Collect_less vec_nth.isCont isCont_const)
    1.51  
    1.52  lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
    1.53    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$i \<le> b) net"
    1.54 @@ -1355,8 +1352,8 @@
    1.55  proof-
    1.56    { fix i::'n
    1.57      have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
    1.58 -      by (cases "P i", simp_all, intro closed_Collect_eq
    1.59 -        continuous_at_component continuous_const) }
    1.60 +      by (cases "P i", simp_all,
    1.61 +        intro closed_Collect_eq vec_nth.isCont isCont_const) }
    1.62    thus ?thesis
    1.63      unfolding Collect_all_eq by (simp add: closed_INT)
    1.64  qed