*To*: Thomas Göthel <tgoethel at cs.tu-berlin.de>*Subject*: Re: [isabelle] Lazy Lists in HOL*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 19 Mar 2007 09:56:04 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20070318115751.11CAAF267@mailhost.cs.tu-berlin.de>*References*: <20070318115751.11CAAF267@mailhost.cs.tu-berlin.de>

* None: the result is the empty list

<http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-304.html> Larry Paulson On 18 Mar 2007, at 12:02, Thomas Göthel wrote:

I wanted to use the LazyList - theory of HOL (LList.thy) from Lawrence Paulson. Unfortunately I didn't find a theory containing the typicalhigher-order functions like filter, zip, etc for "'a llist".Furthermore Imiss a predicate like is_finite for checking finiteness of a lazylist. Isthere such an additional theory or do I have to define these functions myself?Maybe it is possible to use the definitions of SList.thy, doesanybody knowhow?

**References**:**[isabelle] Lazy Lists in HOL***From:*Thomas Göthel

- Previous by Date: Re: [isabelle] Lazy Lists in HOL
- Next by Date: [isabelle] CALL FOR PAPER ACL2 2007
- Previous by Thread: Re: [isabelle] Lazy Lists in HOL
- Next by Thread: [isabelle] TPHOLs 2008: Election Result
- Cl-isabelle-users March 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list