*** empty log message ***
authornipkow
Fri May 11 20:07:00 2007 +0200 (2007-05-11)
changeset 2294042de50e78446
parent 22939 2afc93a3d8f4
child 22941 314b45eb422d
*** empty log message ***
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri May 11 18:49:15 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 11 20:07:00 2007 +0200
     1.3 @@ -2221,6 +2221,10 @@
     1.4  
     1.5  subsubsection {* @{const allpairs} *}
     1.6  
     1.7 +lemma allpairs_conv_concat:
     1.8 + "allpairs f xs ys = concat(map (%x. map (f x) ys) xs)"
     1.9 +by(induct xs) auto
    1.10 +
    1.11  lemma allpairs_append:
    1.12   "allpairs f (xs @ ys) zs = allpairs f xs zs @ allpairs f ys zs"
    1.13  by(induct xs) auto