[isabelle-dev] Word sessions and theories

[Lawrence Paulson]

I totally agree with this point.
Larry

> On 9 Oct 2020, at 00:39, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au> 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”.