[isabelle] Lemmas reuse


please I want to know if I used for example the definition:  "setL2 f A" in
L2_norm.thy , so does this apply all lemmas inside the theory file as
setL2_cong and setL2_triangle_ineq and so on or I have to apply each lemma
in my file?

and another question: in  setL2 f A = sqrt (âiâA. (f i)â2), how can I
substitute i as the definition just include f and A?

Many thanks in advance

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