[isabelle] expanding function composition after induction
I have the theory:
theory test imports Main
definition "F = top"
lemma A: "F (f o g) (n::nat) = top"
lemma B: "F (f o g) (n::nat) = top"
apply (induction n)
The question is why in lemma A, auto fails as expected, while in lemma B
changes (f o g) into (λa. f (g a)). How can I prevent this change?
This archive was generated by a fusion of
Pipermail (Mailman edition) and