--- a/src/HOL/Hyperreal/MacLaurin.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Mar 02 12:06:15 2005 +0100
@@ -99,9 +99,9 @@
prefer 3 apply (simp add: fact_diff_Suc)
prefer 2 apply simp
apply (frule_tac m = m in less_add_one, clarify)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (rule lemma_DERIV_subst)
apply (rule DERIV_add)
apply (rule_tac [2] DERIV_const)
@@ -157,9 +157,9 @@
apply (erule exE)
apply (subgoal_tac "g 0 = 0 & g h =0")
prefer 2
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
apply (cut_tac n = m and k = 1 in sumr_offset2)
- apply (simp add: eq_diff_eq' del: setsum_Suc)
+ apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
prefer 2 apply blast
apply (erule exE)
@@ -178,9 +178,9 @@
apply clarify
apply simp
apply (frule_tac m = ma in less_add_one, clarify)
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
apply (rule allI, rule impI)
apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
@@ -515,7 +515,7 @@
apply (simp (no_asm))
apply (simp (no_asm))
apply (case_tac "n", simp)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)