src/HOL/Transcendental.thy
changeset 56181 2aa0b19e74f3
parent 56167 ac8098b0e458
child 56193 c726ecfb22b6
     1.1 --- a/src/HOL/Transcendental.thy	Mon Mar 17 18:06:59 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 17 19:12:52 2014 +0100
     1.3 @@ -1383,7 +1383,7 @@
     1.4      hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
     1.5        unfolding One_nat_def by auto
     1.6      hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
     1.7 -      unfolding DERIV_iff repos .
     1.8 +      unfolding deriv_def repos .
     1.9      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
    1.10        by (rule DERIV_diff)
    1.11      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
    1.12 @@ -2485,8 +2485,8 @@
    1.13    fix x y
    1.14    assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
    1.15    assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
    1.16 -  have [simp]: "\<forall>x. cos differentiable x"
    1.17 -    unfolding differentiable_def by (auto intro: DERIV_cos)
    1.18 +  have [simp]: "\<forall>x. cos differentiable (at x)"
    1.19 +    unfolding real_differentiable_def by (auto intro: DERIV_cos)
    1.20    from x y show "x = y"
    1.21      apply (cut_tac less_linear [of x y], auto)
    1.22      apply (drule_tac f = cos in Rolle)
    1.23 @@ -2661,8 +2661,8 @@
    1.24    fix a b
    1.25    assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
    1.26    assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
    1.27 -  have [simp]: "\<forall>x. cos differentiable x"
    1.28 -    unfolding differentiable_def by (auto intro: DERIV_cos)
    1.29 +  have [simp]: "\<forall>x. cos differentiable (at x)"
    1.30 +    unfolding real_differentiable_def by (auto intro: DERIV_cos)
    1.31    from a b show "a = b"
    1.32      apply (cut_tac less_linear [of a b], auto)
    1.33      apply (drule_tac f = cos in Rolle)
    1.34 @@ -2949,7 +2949,7 @@
    1.35    apply (rule_tac [4] Rolle)
    1.36    apply (rule_tac [2] Rolle)
    1.37    apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
    1.38 -              simp add: differentiable_def)
    1.39 +              simp add: real_differentiable_def)
    1.40    txt{*Now, simulate TRYALL*}
    1.41    apply (rule_tac [!] DERIV_tan asm_rl)
    1.42    apply (auto dest!: DERIV_unique [OF _ DERIV_tan]