Re: [isabelle] case_names for fun



On 22.02.2012 12:27, John Wickerson wrote:
Thanks Lars. I actually tried that already, but it doesn't work. Below is a snippet of my theory file. After the last line, Isabelle says 'Unknown case: "name1"'.

Yes, you are right. The case_names attribute does not modify lemma, but returns a modified lemma. So

  (induct rule: mk_inner_vertex_inj.induct[case_names name1 name2]

will work, and

  lemmas my_induct_rule
     = mk_inner_vertex_inj.induct[case_names name1, name2]

will work, too.

  -- Lars





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