[isabelle-dev] NEWS

Larry Paulson lp15 at cam.ac.uk
Thu Sep 10 13:39:04 CEST 2015

Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory.

> On 10 Sep 2015, at 12:34, Tobias Nipkow <nipkow at in.tum.de> wrote:
> On 10/09/2015 12:19, Dmitriy Traytel wrote:
>> Hi Florian,
>> while I very much welcome the simplified printing rules and your effort of
>> unifying case_prod/split, I am not sure if adding a third alternative name is
>> the way to go. The situation reminds me of the one depicted in [1].
>> Clearly, case_prod is the "right" name from the perspective of the (co)datatype
>> package.
> Yes, we should return to that name in the end.
> Tobias

More information about the isabelle-dev mailing list