# HG changeset patch
# User nipkow
# Date 1178906820 -7200
# Node ID 42de50e78446109c3740c1389764ab96a7149f52
# Parent  2afc93a3d8f4ceda707f77f233736ee388592ed0
*** empty log message ***

diff -r 2afc93a3d8f4 -r 42de50e78446 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 11 18:49:15 2007 +0200
+++ b/src/HOL/List.thy	Fri May 11 20:07:00 2007 +0200
@@ -2221,6 +2221,10 @@
 
 subsubsection {* @{const allpairs} *}
 
+lemma allpairs_conv_concat:
+ "allpairs f xs ys = concat(map (%x. map (f x) ys) xs)"
+by(induct xs) auto
+
 lemma allpairs_append:
  "allpairs f (xs @ ys) zs = allpairs f xs zs @ allpairs f ys zs"
 by(induct xs) auto