*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 7 Nov 2007 15:39:19 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4731D415.9020008@uni-muenster.de>*References*: <4731B6C9.4040906@uni-muenster.de> <726A4E9C-4CD1-49AE-9CB1-D46CE1C1D731@cam.ac.uk> <4731D415.9020008@uni-muenster.de>

However, this problem mainly seems to affect (f\<circ>g). Larry On 7 Nov 2007, at 15:04, Peter Lammich wrote:

Yes, it is exactly that. And the expansion to "%x. (f\<circ>g) x" wasdone by the induct - method (no idea why, and why only at someplaces).All in all this makes coping with lemmas like list.map_compose rather counter-intuitive. Are there some general guidelines how oneshould/could circumvent stuff like this or do I simply have to livewith it.Many thanks for pointing me to that (I did not even know that termsaredisplayed eta-contracted by default)

**References**:**[isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]***From:*Peter Lammich

**Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]***From:*Lawrence Paulson

**Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]***From:*Peter Lammich

- Previous by Date: Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]
- Next by Date: [isabelle] proving the substitution lemma
- Previous by Thread: Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]
- Next by Thread: [isabelle] proving the substitution lemma
- Cl-isabelle-users November 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