[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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and