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 .
>> Clearly, case_prod is the "right" name from the perspective of the (co)datatype
> Yes, we should return to that name in the end.
More information about the isabelle-dev