*** empty log message ***

--- 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