--- a/src/Doc/Main/Main_Doc.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/Doc/Main/Main_Doc.thy Sun Dec 27 22:07:17 2015 +0100
@@ -228,7 +228,7 @@
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
@{term"Pair a b"} & @{term[source]"Pair a b"}\\
@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
+@{term"A \<times> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"}
\end{tabular}
Pairs may be nested. Nesting to the right is printed as a tuple,