use less_iff_Suc_add instead of less_add_one
authorhuffman
Wed Dec 24 09:26:18 2008 -0800 (2008-12-24)
changeset 29168ff13de554ed0
parent 29167 37a952bb9ebc
child 29169 6a5f1d8d7344
use less_iff_Suc_add instead of less_add_one
src/HOL/MacLaurin.thy
     1.1 --- a/src/HOL/MacLaurin.thy	Wed Dec 24 08:40:16 2008 -0800
     1.2 +++ b/src/HOL/MacLaurin.thy	Wed Dec 24 09:26:18 2008 -0800
     1.3 @@ -77,7 +77,7 @@
     1.4  apply (rule_tac [2] DERIV_pow)
     1.5    prefer 3 apply (simp add: fact_diff_Suc)
     1.6   prefer 2 apply simp
     1.7 -apply (frule_tac m = m in less_add_one, clarify)
     1.8 +apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     1.9  apply (simp del: setsum_op_ivl_Suc)
    1.10  apply (insert sumr_offset4 [of 1])
    1.11  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.12 @@ -150,7 +150,7 @@
    1.13   prefer 2
    1.14   apply clarify
    1.15   apply simp
    1.16 - apply (frule_tac m = ma in less_add_one, clarify)
    1.17 + apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.18   apply (simp del: setsum_op_ivl_Suc)
    1.19  apply (insert sumr_offset4 [of 1])
    1.20  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)