src/Doc/Main/Main_Doc.thy
changeset 63950 cdc1e59aa513
parent 63935 aa1fe1103ab8
child 64267 b9a1486e79be
--- 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}