src/HOL/List.thy
changeset 14591 7be4d5dadf15
parent 14589 feae7b5fd425
child 14770 fe9504ba63d5
     1.1 --- a/src/HOL/List.thy	Fri Apr 16 13:52:43 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Apr 16 15:46:50 2004 +0200
     1.3 @@ -847,6 +847,12 @@
     1.4  apply (case_tac i, auto)
     1.5  done
     1.6  
     1.7 +lemma drop_Suc_conv_tl:
     1.8 +  "!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
     1.9 +apply (induct xs, simp)
    1.10 +apply (case_tac i, auto)
    1.11 +done
    1.12 +
    1.13  lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
    1.14  by (induct n) (auto, case_tac xs, auto)
    1.15