HOL-ex.Bit_Operation_Computations