Re: [isabelle] *_sumC generated by function package



On 21.01.2013 18:13, Walther Neuper wrote:
First steps with the function package were successful.

Now I don't know how to remove a proof obligation containing a function
constant named 'function_id_sumC', where 'function_id' is the function
under consideration:

This is what you get if you unfold function_id_def which is something you would never do in a normal proof.

Using function_id.{simps,induct,cases} should suffice.

  -- Lars





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