It's great to see that people are working with infinite data structures.

`However, there are now three different formalisations of (possibly)
``infinite lists in the AFP: Lazy Lists II by Stefan Friedrich, Infinite
``Lists by David Trachtenherz and Coinductive by myself. At present,
``they are pairwise incompatible, and each of them has a different
``focus: Lazy Lists II focuses on lists over alphabets, Infinite Lists
``on infinite lists, and Coinductive on coinductive definitions and proofs.
``I think it would be great if there was just one theory similar to
``HOL/List that unified these three as far as possible such that future
``users do not have to pick one (or reinvent their own) and relinquish
``the other developments.
`

`Moreover, both Coinductive and Infinite Lists contain additions to
``Nat_Infinity in HOL/Library (theories Coinductive_Nat and Util_NatInf,
``resp.). Interestingly, both of them instantiate the type class minus
``for inat in exactly same way. Alas, no Isabelle session can import
``both because that type classes can be instantiated only once. As
``Util_NatInf's setup for arithmetic is more elaborate than
``Coinductive_Nat's, I suggest to move this to Nat_Infinity in
``Isabelle's library. Is there anyone using Nat_Infinity with other type
``class instantiations, which would break then?
`

`Andreas
`