[isabelle] where to add coding

Hi everyone,
I am new in Isabelle and I would like to implement a proposed proof
technique in it but I don't know where I have to add my code. I am looking
for help.
many thanks,

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