# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1531675342 -3600
# Node ID f33ffa0a27a16e4b8c2630dbe9bf8788b9b29553
# Parent  8094b853a92f7aea8cd7e1e4a8fc4ee221444338
more renaming fixes

diff -r 8094b853a92f -r f33ffa0a27a1 src/Doc/Tutorial/Types/Numbers.thy
--- a/src/Doc/Tutorial/Types/Numbers.thy	Sun Jul 15 16:05:38 2018 +0100
+++ b/src/Doc/Tutorial/Types/Numbers.thy	Sun Jul 15 18:22:22 2018 +0100
@@ -143,8 +143,8 @@
 @{thm[display] mod_add_eq[no_vars]}
 \rulename{mod_add_eq}
 
-@{thm[display] zdiv_zmult1_eq[no_vars]}
-\rulename{zdiv_zmult1_eq}
+@{thm[display] div_mult1_eq[no_vars]}
+\rulename{div_mult1_eq}
 
 @{thm[display] mod_mult_right_eq[no_vars]}
 \rulename{mod_mult_right_eq}