--- a/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:24:50 2009 +0100
+++ b/src/HOL/Docs/MainDoc.thy Mon Mar 09 09:38:36 2009 +0100
@@ -370,6 +370,7 @@
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
\end{supertabular}
???????