List.thy

   map       :: "('a=>'b) => ('a list => 'b list)"
   "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
   filter    :: "['a => bool, 'a list] => 'a list"
   foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
   length    :: "'a list => nat"
+  flat      :: "'a list list => 'a list"
   nth       :: "[nat, 'a list] => 'a"
 
 syntax
   (* list Enumeration *)
   "@list"   :: "args => 'a list"                        ("[(_)]")

   foldl_Nil  "foldl(f,a,[]) = a"
   foldl_Cons "foldl(f,a,x#xs) = foldl(f, f(a,x), xs)"
 primrec length list
   length_Nil  "length([]) = 0"
   length_Cons "length(x#xs) = Suc(length(xs))"
+primrec flat list
+  flat_Nil  "flat([]) = []"
+  flat_Cons "flat(x#xs) = x @ flat(xs)"
 defs
   nth_def "nth(n) == nat_rec(n, hd, %m r xs. r(tl(xs)))"
 end