[isabelle-dev] neg_numeral fallout

Lars Noschinski noschinl at in.tum.de
Fri May 16 12:53:03 CEST 2014

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

More information about the isabelle-dev mailing list