[isabelle-dev] neg_numeral fallout
Lars Noschinski
noschinl at in.tum.de
Fri May 16 16:40:58 CEST 2014
On 16.05.2014 12:53, Lars Noschinski wrote:
> 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.
See now 376604d56b5
-- Lars
More information about the isabelle-dev
mailing list