[isabelle-dev] Notes on datatype_new list

[Lawrence Paulson]

What new users see when they look at the actual definition of lists is not that important. There are many, many situations where the actual definition of something is much more complicated than the idealised version that one would use for teaching. What is necessary is that simple-looking definitions of the old style still continue to work. In most cases, the simple form is all that will be necessary. I have almost never found destructors or discriminators to be useful.

--lcp

> On 26 May 2014, at 11:21, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> Just to be clear on this: the ability to get all of these functions for free is
> marvellous! We are now discussion only the syntactic interface to that
> marvellous functionality, how much is exposed by default, and in particular in
> the defn of list.