diff -r 9f81ab1b7b64 -r 46f3b89b2445 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Tue Apr 08 20:14:36 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Wed Apr 09 05:30:14 2008 +0200
@@ -38,39 +38,6 @@
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     if y then rbl_add ws x else ws)"
 
-lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
-  apply (cases n, clarsimp)
-  apply (cases l, auto)
-  done
-
-lemma take_butlast [rule_format] :
-  "ALL n. n < length l --> take n (butlast l) = take n l"
-  apply (induct l, clarsimp)
-  apply clarsimp
-  apply (case_tac n)
-  apply auto
-  done
-
-lemma butlast_take [rule_format] :
-  "ALL n. n <= length l --> butlast (take n l) = take (n - 1) l"
-  apply (induct l, clarsimp)
-  apply clarsimp
-  apply (case_tac "n")
-   apply safe
-   apply simp_all
-  apply (case_tac "nat")
-   apply auto
-  done
-
-lemma butlast_drop [rule_format] :
-  "ALL n. butlast (drop n l) = drop n (butlast l)"
-  apply (induct l)
-   apply clarsimp
-  apply clarsimp
-  apply safe
-   apply ((case_tac n, auto)[1])+
-  done
-
 lemma butlast_power:
   "(butlast ^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)