# HG changeset patch
# User haftmann
# Date 1476603065 -7200
# Node ID 3d00821444fcdb2ce6d0280bb6df7a8e15f77dc5
# Parent  e7102c40783c65850518f0dcf6a3ab85bc58ec29
avoid references to lemmas designed for prover tools

diff -r e7102c40783c -r 3d00821444fc src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -291,7 +291,7 @@
 
 lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
 
-lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
+lemmas dme = div_mult_mod_eq
 lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
 lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]