[isabelle-dev] Notes on datatype_new list

[Jasmin Christian Blanchette]

Am 26.05.2014 um 10:30 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> I can only agree with what Makarius has observed but would go one step further:
> the new definition of list is truly baroque and unsuitable for beginners, but
> beginners are bound to look at it. Sometimes languages have to reduce complexity
> to cater for novices.

I have been careful to distinguish in my email between what the package provides and the syntax it gives for it. Would it be possible to articulate your criticism more precisely along those axes?

Jasmin