# HG changeset patch
# User huffman
# Date 1230139578 28800
# Node ID ff13de554ed0337f5c45e2f3648e8e4a67c26334
# Parent  37a952bb9ebcca4914a4e5518f7b6e54a779ba49
use less_iff_Suc_add instead of less_add_one

diff -r 37a952bb9ebc -r ff13de554ed0 src/HOL/MacLaurin.thy
--- 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)