*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] recursive functions and set comprehension*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Tue, 26 Sep 2006 10:50:13 +0200*Cc*: Dimitrios Vytiniotis <dimitriv at cis.upenn.edu>, isabelle-users at cl.cam.ac.uk*In-reply-to*: <4518E779.5090705@in.tum.de>*References*: <45182AE7.7080309@cis.upenn.edu> <4518E779.5090705@in.tum.de>*User-agent*: Thunderbird 1.5 (X11/20060113)

Dimitrios,

Hello all, consider the (admittedly strange) fragment: datatype tm = Z | S "tm" consts foo :: "tm => tm set" recdef foo "measure size" "foo x = { Z. (x = Z) } \<union> { (S x1) | x1. x = S x1 /\ x1 : (foo x1) }";

Alex

**References**:**[isabelle] recursive functions and set comprehension***From:*Dimitrios Vytiniotis

**Re: [isabelle] recursive functions and set comprehension***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] recursive functions and set comprehension
- Next by Date: Re: [isabelle] LaTeX document
- Previous by Thread: Re: [isabelle] recursive functions and set comprehension
- Next by Thread: [isabelle] Functional Relations
- Cl-isabelle-users September 2006 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