--- a/src/Doc/Main/Main_Doc.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Mon Sep 26 07:56:54 2016 +0200
@@ -325,9 +325,9 @@
@{const divide} & @{typeof divide}\\
@{const abs} & @{typeof abs}\\
@{const sgn} & @{typeof sgn}\\
-@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
-@{const Rings.divide} & @{typeof Rings.divide}\\
-@{const div_class.mod} & @{typeof "div_class.mod"}\\
+@{const Rings.dvd} & @{typeof Rings.dvd}\\
+@{const divide} & @{typeof divide}\\
+@{const modulo} & @{typeof modulo}\\
\end{supertabular}
\subsubsection*{Syntax}