Re: [isabelle] recdef problem

On Friday 16 September 2005 20:56, Nicole Rauch wrote:

> (hints recdef_simp add: rssem_h_term1)
> But still Isabelle gives me the same "Bad final proof state". How can
> I convince Isabelle to accept the lemma as proof for the remaining goal?
> Thanks for any hints


(hints intro: rssem_h_term1 [rule_format])


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