[isabelle-dev] Notes on datatype_new list

[Tobias Nipkow]

The definition of list should look like before.

Tobias


On 26/05/2014 10:59, Jasmin Christian Blanchette wrote:
> 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
>