diff -r 9b403e123c1b -r 2740293cc458 List.thy --- a/List.thy Wed Feb 08 14:06:37 1995 +0100 +++ b/List.thy Mon Feb 13 15:12:08 1995 +0100 @@ -23,6 +23,7 @@ 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 @@ -74,6 +75,9 @@ 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