--- a/src/HOL/List.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/List.thy Thu Sep 22 23:56:15 2005 +0200
@@ -264,7 +264,7 @@
lemma length_induct:
"(!!xs. \<forall>ys. length ys < length xs --> P ys ==> P xs) ==> P xs"
-by (rule measure_induct [of length]) rules
+by (rule measure_induct [of length]) iprover
subsubsection {* @{text length} *}
@@ -550,7 +550,7 @@
by(blast dest:map_injective)
lemma inj_mapI: "inj f ==> inj (map f)"
-by (rules dest: map_injective injD intro: inj_onI)
+by (iprover dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) ==> inj f"
apply (unfold inj_on_def, clarify)
@@ -977,6 +977,9 @@
apply (auto split:nat.split)
done
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
+by(induct xs)(auto simp:neq_Nil_conv)
+
subsubsection {* @{text take} and @{text drop} *}