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.
---Elsa

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
    

Try: 

(hints intro: rssem_h_term1 [rule_format])

   Norbert 
  


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