[isabelle-dev] Notes on datatype_new list

[Florian Haftmann]

Hi again,
> datatype_new 'a list =
> Nil (defaults un_Cons2: "[]") ("[]")
> | Cons 'a "'a list" (infixr "#" 65)
> 
> abbreviation "map ≡ map_list"
> abbreviation "set ≡ set_list"
> abbreviation "list_all2 ≡ rel_list"
> abbreviation "hd ≡ un_Cons1"
> abbreviation "tl ≡ un_Cons2"

this would make sense if you were to abandon the lhses in favour of the
rhses in the mid future, which, as I dare to state plainly, you don't
want to do.  Duplication is a migration solution, not a solution in itself.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140526/e0af4f2e/attachment.sig>