diff -r 5a29dbf4c155 -r d9fe85d3d2cd doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Fri Jan 06 10:19:49 2012 +0100 +++ b/doc-src/Main/Docs/Main_Doc.thy Fri Jan 06 10:19:49 2012 +0100 @@ -495,8 +495,9 @@ @{const List.drop} & @{typeof List.drop}\\ @{const List.dropWhile} & @{typeof List.dropWhile}\\ @{const List.filter} & @{typeof List.filter}\\ +@{const List.fold} & @{typeof List.fold}\\ +@{const List.foldr} & @{typeof List.foldr}\\ @{const List.foldl} & @{typeof List.foldl}\\ -@{const List.foldr} & @{typeof List.foldr}\\ @{const List.hd} & @{typeof List.hd}\\ @{const List.last} & @{typeof List.last}\\ @{const List.length} & @{typeof List.length}\\