src/HOL/MacLaurin.thy
changeset 56181 2aa0b19e74f3
parent 51489 f738e6dbd844
child 56193 c726ecfb22b6
     1.1 --- a/src/HOL/MacLaurin.thy	Mon Mar 17 18:06:59 2014 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Mon Mar 17 19:12:52 2014 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4      by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
     1.5  
     1.6    have differentiable_difg:
     1.7 -    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
     1.8 +    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)"
     1.9      by (rule differentiableI [OF difg_Suc [rule_format]]) simp
    1.10  
    1.11    have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
    1.12 @@ -135,7 +135,7 @@
    1.13        show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
    1.14        show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
    1.15          by (simp add: isCont_difg n)
    1.16 -      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
    1.17 +      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable (at x)"
    1.18          by (simp add: differentiable_difg n)
    1.19      qed
    1.20    next
    1.21 @@ -149,7 +149,7 @@
    1.22          using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
    1.23        show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
    1.24          using `t < h` `Suc m' < n` by (simp add: isCont_difg)
    1.25 -      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
    1.26 +      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)"
    1.27          using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
    1.28      qed
    1.29      thus ?case