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 <nip...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
