changeset 22551 | e52f5400e331 |
parent 22539 | ad3bd3d6ba8a |
child 22633 | a47e4fd7ebc1 |
--- 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} *}