# [isabelle] eta-contracted definitions and unfolding

Hello,

`I've got a few definitions that are supposed to be partially applied,
``and unfolding them when they are eta-contracted and unsaturated fails
``(silently in the case of 'unfolding'). I am surprised this doesn't
``work in Isabelle2008, e.g.:
`
theory t
imports Main
begin
constdefs
f :: "nat ⇒ nat ⇒ nat"
"f x y ≡ x + y"
g :: "nat ⇒ nat ⇒ nat"
"g x y ≡ y + x"
lemma "f = g"
unfolding f_def g_def
sorry
definition "f' x y ≡ x + y"
definition "g' x y ≡ y + x"
lemma "f' = g'"
unfolding f_def g_def
sorry
end
Has Isabelle always behaved like this?

`In my particular cases I can use extensionality, but I'm keen to know
``if there are alternatives.
`
Thanks,
Peter.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*