[isabelle-dev] Word sessions and theories

Lawrence Paulson lp15 at cam.ac.uk
Fri Oct 9 13:40:45 CEST 2020


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”. 



More information about the isabelle-dev mailing list