[isabelle] lemma tempates



Hi!

I have several functions for all of which I need to prove some trivial lemmas.
For example 

lemma f0: "f 0 = 0"
lemma g0: "g 0 = 0"
lemma h0: "h 0 = 0"

These lemmas might be used further in more complex proofs so I would like them to
be named. As I add more functions I will need to instantiate these lemmas
for newly added ones easily. What would be the best way to do this? 

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva





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