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


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