[isabelle-dev] NEWS

[Larry Paulson]

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

> 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