On 22.02.2012 12:09, John Wickerson wrote:
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?
You can do this with: declare f.induct[case_names name1 name2] -- Lars