more renaming fixes
authorpaulson <lp15@cam.ac.uk>
Sun, 15 Jul 2018 18:22:22 +0100
changeset 68636 f33ffa0a27a1
parent 68635 8094b853a92f
child 68637 ec8c7c9459e0
more renaming fixes
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}