[isabelle-dev] Notes on datatype_new list
nipkow at in.tum.de
Mon May 26 11:02:05 CEST 2014
The definition of list should look like before.
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?
More information about the isabelle-dev