Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use less_iff_Suc_add instead of less_add_one
authorhuffman
Wed, 24 Dec 2008 09:26:18 -0800
changeset 29168 ff13de554ed0
parent 29167 37a952bb9ebc
child 29169 6a5f1d8d7344
use less_iff_Suc_add instead of less_add_one
src/HOL/MacLaurin.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle