*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 18 Dec 2013 19:40:43 -0600*In-reply-to*: <52B227C7.6070607@gmx.com>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <52AC4D87.9030304@gmx.com> <op.w723lrn9ule2fv@cardamome> <52B227C7.6070607@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 12/18/2013 4:55 PM, Gottfried Barrow wrote:

theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False" by(auto) (*EXAMPLE: This example, similar to yours, will be made concrete withsumXp.*) theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10"

Regards, GB

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

- Previous by Date: [isabelle] Instantiating type classes
- Next by Date: [isabelle] [SOLVED] jedit mouse offset/menu bug with fullscreen window managers
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 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