[isabelle-dev] Notes on datatype_new list

Jasmin Blanchette jasmin.blanchette at gmail.com
Mon May 26 11:07:04 CEST 2014

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


More information about the isabelle-dev mailing list