| changeset 60352 | d46de31a50c4 |
| parent 59807 | 22bc39064290 |
| child 60429 | d3d1e185cd63 |
--- a/src/HOL/Word/Word.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Word/Word.thy Mon Jun 01 18:59:21 2015 +0200 @@ -307,7 +307,7 @@ by (metis bintr_ariths(4)) definition - word_div_def: "a div b = word_of_int (uint a div uint b)" + word_div_def: "divide a b = word_of_int (uint a div uint b)" definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)"