[isabelle] case_names for fun



Dear Isabelle,

I have a function f defined recursively using "fun". When I do induction using f.induct, the case names are "1" and "2". How can I set them to more useful names?

Thank you,
John




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