# HG changeset patch
# User nipkow
# Date 1379499370 -7200
# Node ID 705f0b728b1b67b957a077c35ba3a4426d1ad47c
# Parent  63892cfef47ff91901500f09d6f7ece5c0288feb
added and tuned lemmas

diff -r 63892cfef47f -r 705f0b728b1b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 18 00:11:15 2013 +0200
+++ b/src/HOL/List.thy	Wed Sep 18 12:16:10 2013 +0200
@@ -710,9 +710,15 @@
 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
 by (induct xs) auto
 
+lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
+by (cases xs) auto
+
+lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"
+by (cases xs) auto
+
 lemma length_induct:
   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
-by (rule measure_induct [of length]) iprover
+by (fact measure_induct)
 
 lemma list_nonempty_induct [consumes 1, case_names single cons]:
   assumes "xs \<noteq> []"