Mercurial Mercurial > hg > pip / 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.
another simplification
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 13 Jan 2016 15:22:14 +0000
changeset 72 3fa70b12c117
parent 71 04caf0ccb3ae
child 73 b0054fb0d1ce
another simplification
Moment.thy file | annotate | diff | comparison | revisions 
--- a/Moment.thy	Wed Jan 13 15:16:59 2016 +0000
+++ b/Moment.thy	Wed Jan 13 15:22:14 2016 +0000
@@ -146,9 +146,8 @@
 lemma moment_Suc_tl:
   assumes "Suc i \<le> length s"
   shows "tl (moment (Suc i) s) = moment i s"
-  using assms unfolding moment_def
-sorry
-
+  using assms unfolding moment_def rev_take
+by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
 
 lemma moment_plus:
   assumes "Suc i \<le> length s"
pip