On 16.05.2014 12:30, Gerwin Klein wrote: > Looks ok, but what about all the other operators? (shift, rotate, etc) As far as I can see, shift and rotate don't have their own lemmas for evaluating numerals, so the demise of neg_numerals shouldn't have introduced a regression there. -- Lars