# HG changeset patch
# User haftmann
# Date 1175264340 -7200
# Node ID e52f5400e331c89dff0d57e3fe877e8fe57c89a9
# Parent  c5039bee260284be2c879357a86d54963d98b0ec
paraphrasing equality

diff -r c5039bee2602 -r e52f5400e331 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Mar 30 16:18:59 2007 +0200
+++ b/src/HOL/List.thy	Fri Mar 30 16:19:00 2007 +0200
@@ -1601,6 +1601,10 @@
   apply (case_tac y, auto)
   done
 
+lemma list_all2_eq:
+  "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
+  by (induct xs ys rule: list_induct2') auto
+
 
 subsubsection {* @{text foldl} and @{text foldr} *}