[isabelle] limiting unfolding using definitions



Hello,

I have a goal "f <= g" where f, g:: A => B => C.
I want to unfold the goal using le_fun_def only once:
"!! x . f x <= g x"
How can I achieve this goal? If I apply (unfold le_fun_def)
the goal becomes: "!! x y . f x y <= g x y".

I want to avoid re-typing (copying) the expressions f and g.

Best regards,

Viorel





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