--- a/src/HOL/List.thy Fri Feb 24 22:46:44 2012 +0100
+++ b/src/HOL/List.thy Sat Feb 25 09:07:37 2012 +0100
@@ -2342,12 +2342,8 @@
by (simp add: list_all2_conv_all_nth)
lemma list_all2_update_cong:
- "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_conv_all_nth nth_list_update)
-
-lemma list_all2_update_cong2:
- "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_lengthD list_all2_update_cong)
+ "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
+by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
lemma list_all2_takeI [simp,intro?]:
"list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"