[isabelle-dev] Notes on datatype_new list

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Mon May 26 10:59:05 CEST 2014

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?


More information about the isabelle-dev mailing list