# [isabelle] Kind of generic lemmas: possible?

Hi people out there,
Here is a naive attempt I've just made for testing. It is self explanatory:
lemma obligation: "f x y ⟹ f y x" sorry
fun equal :: "nat ⇒ nat ⇒ bool"
where "equal x y = (x = y)"
thm obligation [where f = equal]
lemma equal_obligation: obligation [where f = equal]

`The “thm” line is OK, but not the last lemma. Is this just stupid in an
``Isabelle context or is there another way to achieve the same purpose?
`
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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