1.1 --- a/src/HOL/List.thy	Wed Sep 18 00:11:15 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Sep 18 12:16:10 2013 +0200
     1.3 @@ -710,9 +710,15 @@
     1.4  lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
     1.5  by (induct xs) auto
     1.6  
     1.7 +lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
     1.8 +by (cases xs) auto
     1.9 +
    1.10 +lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
    1.11 +by (cases xs) auto
    1.12 +
    1.13  lemma length_induct:
    1.14    "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
    1.15 -by (rule measure_induct [of length]) iprover
    1.16 +by (fact measure_induct)
    1.17  
    1.18  lemma list_nonempty_induct [consumes 1, case_names single cons]:
    1.19    assumes "xs \<noteq> []"