[isabelle-dev] Notes on datatype_new list

[Jasmin Blanchette]

Am 26.05.2014 um 11:02 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> The definition of list should look like before.

I don't see how this is an option. This would result in the following duplicate constants:

    map_list vs. map
    set_list vs. set
    rel_list vs. forall_list2
    un_Cons1 vs. hd
    un_Cons2 vs. tl

Jasmin