I totally agree with this point. Larry > On 9 Oct 2020, at 00:39, Klein, Gerwin (Data61, Kensington NSW) > <[email protected]> wrote: > > the desire to replace operations like lsb, msb, etc with existing operations. > That would be counter productive. If they can be made abbreviations on the > word type, that is fine, and should probably be done, but the names are > important. Programmers know what “lsb" ist, but will have to really think > about this being equivalent to “odd”.
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
