# [isabelle] Congruence rule for Let

Hi all,

`using the function package, I'd like to define a function whose
``definition contains a number of Let expressions. In the generated
``induction rule, a term "Let t (%x. y)" yields the induction hypothesis
``"!!x. x = t ==> P (y x)"
``However, I would like to get "P (y t)" directly. How do I have to change
``the congruence rule for Let to achieve this?
`
I tried two alternatives with fundef_cong:
- "[| M = N; f N = g N |] ==> Let M f = Let N g" raises an exception:
*** exception THM 1 raised (line 421 of "drule.ML"): COMP
*** At command "function".

`- "[| M = N; f M = g N |] ==> Let M f = Let N g" eliminates the
``quantifier, but produces far to many induction hypotheses.
`
What is the right congruence rule for this?
Andreas

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