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
= mk_inner_vertex_inj.induct[case_names name1, name2]
will work, too.
This archive was generated by a fusion of
Pipermail (Mailman edition) and