src/HOL/NthRoot.thy
changeset 56381 0556204bc230
parent 56371 fb9ae0727548
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/NthRoot.thy	Thu Apr 03 17:16:02 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Thu Apr 03 17:56:08 2014 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4    qed
     1.5  next
     1.6    show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
     1.7 -    by  (auto intro!: DERIV_intros)
     1.8 +    by  (auto intro!: derivative_eq_intros simp: real_of_nat_def)
     1.9    show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
    1.10      using n x by simp
    1.11  qed (rule isCont_real_root)
    1.12 @@ -471,8 +471,8 @@
    1.13    using DERIV_real_sqrt_generic by simp
    1.14  
    1.15  declare
    1.16 -  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.17 -  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.18 +  DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
    1.19 +  DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
    1.20  
    1.21  lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
    1.22  apply auto