Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid references to lemmas designed for prover tools
authorhaftmann
Sun, 16 Oct 2016 09:31:05 +0200
changeset 64245 3d00821444fc
parent 64244 e7102c40783c
child 64246 15d1ee6e847b
avoid references to lemmas designed for prover tools
src/HOL/Word/Word_Miscellaneous.thy file | annotate | diff | comparison | revisions 
--- 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]
isabelle