# HG changeset patch
# User Andreas Lochbihler
# Date 1403675361 -7200
# Node ID 52dfde98be4adc8bc262d4b0f1d7d4babe2af803
# Parent  7938a6881b26dab73e9315840c51b275cbc8c794# Parent  e02fcb7e63c377e6842c529434f784b1a78060a1
merged

diff -r 7938a6881b26 -r 52dfde98be4a src/HOL/List.thy
--- 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} *}