--- a/Moment.thy	Wed Jan 13 15:22:14 2016 +0000
+++ b/Moment.thy	Wed Jan 13 23:39:59 2016 +0800
@@ -147,14 +147,14 @@
   assumes "Suc i \<le> length s"
   shows "tl (moment (Suc i) s) = moment i s"
   using assms unfolding moment_def rev_take
-by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
-
+  by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
+  
 lemma moment_plus:
   assumes "Suc i \<le> length s"
   shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)"
 proof -
-  have "(moment (Suc i) s) \<noteq> []"
-  using assms by (auto simp add: moment_def)
+  have "(moment (Suc i) s) \<noteq> []" using assms 
+    by (simp add:moment_def rev_take)
   hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) #  tl (moment (Suc i) s)"
     by auto
   with moment_Suc_tl[OF assms]