src/HOL/Word/BinOperations.thy
changeset 25510 38c15efe603b
parent 25112 98824cc791c0
child 25762 c03e9d04b3e4