--- a/src/HOL/MacLaurin.thy Wed Dec 24 08:40:16 2008 -0800
+++ b/src/HOL/MacLaurin.thy Wed Dec 24 09:26:18 2008 -0800
@@ -77,7 +77,7 @@
apply (rule_tac [2] DERIV_pow)
prefer 3 apply (simp add: fact_diff_Suc)
prefer 2 apply simp
-apply (frule_tac m = m in less_add_one, clarify)
+apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
@@ -150,7 +150,7 @@
prefer 2
apply clarify
apply simp
- apply (frule_tac m = ma in less_add_one, clarify)
+ apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)