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]
```