src/HOL/NthRoot.thy
changeset 49753 a344f1a21211
parent 44349 f057535311c5
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/NthRoot.thy	Wed Oct 10 15:01:20 2012 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Oct 10 15:17:40 2012 +0200
     1.3 @@ -398,9 +398,9 @@
     1.4  
     1.5  lemma DERIV_real_root_generic:
     1.6    assumes "0 < n" and "x \<noteq> 0"
     1.7 -  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
     1.8 -  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
     1.9 -  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    1.10 +    and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    1.11 +    and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
    1.12 +    and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    1.13    shows "DERIV (root n) x :> D"
    1.14  using assms by (cases "even n", cases "0 < x",
    1.15    auto intro: DERIV_real_root[THEN DERIV_cong]