[isabelle] lemma tempates


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? 


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.