src/HOL/NthRoot.thy
changeset 56371 fb9ae0727548
parent 55967 5dadc93ff3df
child 56381 0556204bc230
     1.1 --- a/src/HOL/NthRoot.thy	Wed Apr 02 18:35:02 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Apr 02 18:35:07 2014 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4    assume n: "0 < n"
     1.5    let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n"
     1.6    have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
     1.7 -    using n by (intro continuous_on_If continuous_on_intros) auto
     1.8 +    using n by (intro continuous_on_If continuous_intros) auto
     1.9    then have "continuous_on UNIV ?f"
    1.10      by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
    1.11    then have [simp]: "\<And>x. isCont ?f x"
    1.12 @@ -275,7 +275,7 @@
    1.13    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
    1.14    unfolding continuous_def by (rule tendsto_real_root)
    1.15    
    1.16 -lemma continuous_on_real_root[continuous_on_intros]:
    1.17 +lemma continuous_on_real_root[continuous_intros]:
    1.18    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
    1.19    unfolding continuous_on_def by (auto intro: tendsto_real_root)
    1.20  
    1.21 @@ -454,7 +454,7 @@
    1.22    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
    1.23    unfolding sqrt_def by (rule continuous_real_root)
    1.24    
    1.25 -lemma continuous_on_real_sqrt[continuous_on_intros]:
    1.26 +lemma continuous_on_real_sqrt[continuous_intros]:
    1.27    "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
    1.28    unfolding sqrt_def by (rule continuous_on_real_root)
    1.29