src/HOL/MacLaurin.thy
 changeset 56181 2aa0b19e74f3 parent 51489 f738e6dbd844 child 56193 c726ecfb22b6
```--- a/src/HOL/MacLaurin.thy	Mon Mar 17 18:06:59 2014 +0100
+++ b/src/HOL/MacLaurin.thy	Mon Mar 17 19:12:52 2014 +0100
@@ -116,7 +116,7 @@
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp

have differentiable_difg:
-    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
+    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)"
by (rule differentiableI [OF difg_Suc [rule_format]]) simp

have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
@@ -135,7 +135,7 @@
show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
-      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
+      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable (at x)"