Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]
At the moment it isn't easy to tell whether terms are eta-contracted
or not, and if you reset the flag, terms can become unreadable.
However, this problem mainly seems to affect (f\<circ>g).
On 7 Nov 2007, at 15:04, Peter Lammich wrote:
Yes, it is exactly that. And the expansion to "%x. (f\<circ>g) x" was
done by the induct - method (no idea why, and why only at some
All in all this makes coping with lemmas like list.map_compose rather
counter-intuitive. Are there some general guidelines how one
should/could circumvent stuff like this or do I simply have to live
Many thanks for pointing me to that (I did not even know that terms
displayed eta-contracted by default)
This archive was generated by a fusion of
Pipermail (Mailman edition) and