Re: [isabelle] case_names for fun



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





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