Re: [isabelle] recdef problem

I tried out this suggestion on one of my problems and it didn't change anything.  I get teh same "bad final proof state" as before.

Norbert Schirmer wrote:
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.