# 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