[isabelle] Lazy Lists in HOL



Hello,
I wanted to use the LazyList - theory of HOL (LList.thy) from Lawrence
Paulson. Unfortunately I didn't find a theory containing the typical
higher-order functions like filter, zip, etc for "'a llist". Furthermore I
miss a predicate like is_finite for checking finiteness of a lazy list. Is
there such an additional theory or do I have to define these functions
myself?
Maybe it is possible to use the definitions of SList.thy, does anybody know
how?

Bye,
Thomas  






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