[isabelle] lemma tempates
I have several functions for all of which I need to prove some trivial lemmas.
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?
CMU ECE PhD student
This archive was generated by a fusion of
Pipermail (Mailman edition) and