src/HOL/Transcendental.thy
changeset 55417 01fbfb60c33e
parent 54576 e877eec2b698
child 55719 cdddd073bff8
     1.1 --- a/src/HOL/Transcendental.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -624,6 +624,7 @@
     1.4         (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
     1.5        apply (rule ext)
     1.6        apply (case_tac "n", simp)
     1.7 +      apply (rename_tac nat)
     1.8        apply (case_tac "nat", simp)
     1.9        apply (simp add: r_neq_0)
    1.10        done
    1.11 @@ -2710,7 +2711,8 @@
    1.12  apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
    1.13   prefer 2 apply (erule LeastI)
    1.14  apply (case_tac "LEAST m::nat. x < real m * y", simp)
    1.15 -apply (subgoal_tac "~ x < real nat * y")
    1.16 +apply (rename_tac m)
    1.17 +apply (subgoal_tac "~ x < real m * y")
    1.18   prefer 2 apply (rule not_less_Least, simp, force)
    1.19  done
    1.20