diff -r 5e9de4faef98 -r d3d1e185cd63 src/Doc/Tutorial/Misc/appendix.thy
--- a/src/Doc/Tutorial/Misc/appendix.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/Doc/Tutorial/Misc/appendix.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -14,8 +14,8 @@
 @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
 @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
 @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
-@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
-@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
+@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\
+@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\
 @{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
 @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
 @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\