[isabelle] Coinductive_List and LList/LFilter



Hi all,

there are two formalisations of coinductive lists in Isabelle/HOL 2009:
Library/Coinductive_List and Induct/LList, Induct/LFilter.

When I want to use coinductive lists, which one is recommended?
Are there any libraries with additional functions for either of them available (with functions like zip, set, list_all2 in List.thy)?

Regards,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.