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

Try: 

(hints intro: rssem_h_term1 [rule_format])

   Norbert 





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