--- a/src/HOL/List.thy Tue Jun 24 15:49:20 2014 +0200
+++ b/src/HOL/List.thy Wed Jun 25 07:49:21 2014 +0200
@@ -2708,6 +2708,8 @@
"xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
+lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
+by(auto simp add: list_all2_conv_all_nth set_conv_nth)
subsubsection {* @{const List.product} and @{const product_lists} *}