Re: [isabelle] recdef problem



I had this same kind of problem back in the spring, and it was suggested that I try the following:
 (hints intro!: rssem_h_term1)
using intro! rather than simp

Indeed, intro! did the trick (but not intro without the exclamation mark).

Thanks for all the helpful suggestions

Nicole

--
"Never in the field of software development was so much owed by so
many to so few lines of code" -- Martin Fowler about JUnit

Attachment: PGP.sig
Description: Signierter Teil der Nachricht



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